proposition: Lemma quot_eq : forall a b c q1 r1 q2 r2 : nat, a = b -> is_div a c q1 r1 -> is_div b c q2 r2 -> q1 = q2.
proof: Proof. intros a b c q1 r1 q2 r2 H H0 H1; apply div_unic_q with (1 := H0) (r2 := r2). rewrite H; auto. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)