Level: Lib Thy Top: 2
Hypotheses:

  1. q :

  2. (0 = 0)

Conclusion:

(q-1) + (q-1)


Applied Tactic: Auto
Generated subgoals:

None