d q1 q2 r1 r2 : r1 < d -> r2 < d -> d * q1 + r1 = d * q2 + r2 -> q1 = q2 /\ r1 = r2. Proof. intros H1 H2 p. destruct (nat_trichotomy q1 q2) as [[q | q] | q]. - contradiction (nat_div_mod_unique_helper d q1 q2 r1 r2). - split; trivial. destruct q. by apply isinj_nat_add_l in p. - by contradiction (nat_div_mod_unique_helper d q2 q1 r2 r1). Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes