proposition: Lemma eucl_div_unique b q1 r1 q2 r2 : b > r1 -> b > r2 -> q1 * b + r1 = q2 * b + r2 -> q1 = q2 /\ r1 = r2.
proof: Proof. intros. assert ((q1-q2)*b=r2-r1). nia. assert ((q2-q1)*b=r1-r2). rewrite Nat.mul_sub_distr_r. clear H2; lia. destruct (le_gt_dec r1 r2). destruct (eq_nat_dec r1 r2). subst. rewrite Nat.sub_diag in *. nia. assert (r2 - r1 < b). clear -H H0; lia. rewrite <- H2 in H4. rewrite <- (Nat.mul_1_l b) in H4 at -1. ded (mult_lt_r_elim H4). assert (q1=q2). clear H H0 H1 H3 H4; lia. subst q2; clear H2 H3 H4 H5. lia. assert (r1 - r2 < b). clear -H H0; lia. rewrite <- H3 in H4. rewrite <- (Nat.mul_1_l b) in H4 at -1. ded (mult_lt_r_elim H4). assert (q1=q2). clear H H0 H1 H2 H4; lia. subst q2; clear H2 H3 H4 H5. lia. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)