proposition: Lemma div_eucl_unique : forall (a b : nat) (q q' r r' : nat), a = q * b + r -> a = q' * b + r' -> b > r -> b > r' -> q = q' /\ r = r'.
proof: Proof. intros a b q q' r r' Hdiv Hdiv' Hrem Hrem'. assert (q_eq : q = q'). { case lt_eq_lt_dec with q q'; [intro Hq; case Hq; clear Hq | ]; intro Hin. case div_not_qlt with a b q q' r r'; assumption. assumption. case div_not_qlt with a b q' q r' r; assumption. } split; try assumption. apply Nat.add_cancel_l with (q * b). transitivity a; congruence. Qed.
imports: Coq(Arith Lia )