Level: Lib Thy Top: 1
Hypotheses:

  1. q :

  2. n1 :

  3. n2 :

  4. r1 : (qn1)

  5. r2 : (qn2)

  6. (qn1) + r1 = (qn2) + r2

Conclusion:

n1 = n2 r1 = r2

Applied Tactic: Assert n1 = n2 THENM Auto
Generated subgoals:

1. n1 = n2

2. r1 = r2