Level:
Lib
Thy
Top
:
2
Hypotheses:
q :
a :
0 < a
n:
.
(q
n
)
a - 1 <
(q
n + 1
)
Conclusion:
n:
.
(q
n
)
a <
(q
n + 1
)
Applied Tactic:
D 4
Generated subgoals:
1
.
n:
.
(q
n
)
a <
(q
n + 1
)
n:. 
(q
n
) 
a - 1 < (qn + 1)
n:. (qn) a < (qn + 1)n:. (qn) a < (qn + 1)