proposition: Lemma divmod_unicity k k' q r r' : r < q -> r' < q -> k * q + r = k' * q + r' -> k = k' /\ r = r'.
proof: Proof. intros h h' e. destruct (Compare_dec.lt_eq_lt_dec k k') as [[i|i]|i]. apply False_rec. assert (e2 : k * q + r - k * q = k' * q + r' - k * q). lia. rewrite add_sub, swap_add_sub, <- PeanoNat.Nat.mul_sub_distr_r in e2. nia. nia. lia. apply False_rec. assert (e2 : k * q + r - k' * q = k' * q + r' - k' * q). lia. rewrite add_sub, swap_add_sub, <- PeanoNat.Nat.mul_sub_distr_r in e2. nia. nia. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat