proposition: Lemma div_unic_q : forall a b q1 q2 r1 r2 : nat, is_div a b q1 r1 -> is_div a b q2 r2 -> q1 = q2.
proof: Proof. intros a b q1 q2 r1 r2 (H0, H1) (H2, H3). case (Nat.le_gt_cases q1 q2); intros H4. case (proj1 (Nat.lt_eq_cases _ _) H4); auto; clear H4; intros H4. Contradict H0; auto; apply Nat.le_ngt. apply (fun p n m : nat => Nat.add_le_mono_l n m p) with (q1 * b). rewrite <- H1; rewrite H3; auto with arith. apply Nat.le_trans with (q2 * b + 0); auto with arith. replace (q1 * b + b) with (S q1 * b); [ repeat rewrite (fun x => Nat.mul_comm x b) | simpl in |- * ]; auto with arith. Contradict H2; auto; apply Nat.le_ngt. apply (fun p n m : nat => Nat.add_le_mono_l n m p) with (q2 * b). rewrite <- H3; rewrite H1; auto with arith. apply Nat.le_trans with (q1 * b + 0); auto with arith. replace (q2 * b + b) with (S q2 * b); [ repeat rewrite (fun x => Nat.mul_comm x b) | simpl in |- * ]; auto with arith. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)