Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

n:. r1,r2:n. q1,q2:. r1 + q1 * n = r2 + q2 * n r1 = r2 q1 = q2

Applied Tactic: UnivCD THENW Auto
Generated subgoals:

1. r1 = r2 q1 = q2