Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

q:. a:. n:. (qn) a < (qn + 1)

Applied Tactic: D 0 THENW Auto THEN D 0 THENW Auto THEN NatInd 2
Generated subgoals:

1. n:. (qn) 0 < (qn + 1)

2. n:. (qn) a < (qn + 1)