Level:
Lib
Thy
Top
:
1
Hypotheses:
q :
Conclusion:
n:
.
(q
n
)
0 <
(q
n + 1
)
Applied Tactic:
With
0
(D 0) THENW Auto THEN D 0 THEN RecUnfold `geom_series` 0 THEN Reduce 0
Generated subgoals:
1
. 0
0
2
. 0 <
(q
0
) + (q
0)
n:. 
(q
n
) 
0 < (qn + 1)
0
(D 0) THENW Auto THEN D 0 THEN RecUnfold `geom_series` 0 THEN Reduce 0 0(q0) + (q0)