proposition: Lemma div_unic_r : forall a b q1 q2 r1 r2 : nat, is_div a b q1 r1 -> is_div a b q2 r2 -> r1 = r2.
proof: Proof. intros a b q1 q2 r1 r2 (H0, H1) (H2, H3). apply Nat.add_cancel_l with (q1 * b). rewrite <- H1; rewrite H3; rewrite (div_unic_q a b q1 q2 r1 r2); try split; auto with arith. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)