Level: Lib Thy Top: 1
Hypotheses:

  1. n :

  2. r1 : n

  3. r2 : n

  4. q1 :

  5. q2 :

  6. r1 + q1 * n = r2 + q2 * n

Conclusion:

r1 = r2 q1 = q2

Applied Tactic: Assert r1 = r2
Generated subgoals:

1. r1 = r2

2. r1 = r2 q1 = q2