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