Level:
Lib
Thy
Top
:
4
Hypotheses:
q :
n :
0 < n
(q
n - 1
)
(n = 0)
Conclusion:
(q
n - 1
) + (q
n - 1)
Applied Tactic:
BLemma `nat_add` THENA Auto
Generated subgoals:
None
(q
n - 1
) 
(n = 0)
(qn - 1) + (qn - 1)