Level:
Lib
Thy
Top
:
3
Hypotheses:
q :
n :
0 < n
(q
n - 1
)
n = 0
Conclusion:
0
Applied Tactic:
Auto
Generated subgoals:
None
(q
n - 1
) 
0