proposition: Lemma euclid_unique n: lt 0 n -> forall x y x' y', lt x n -> lt x' n -> y*n+x = y'*n+x' -> y=y' /\ x=x'.
proof: Proof. intros Hn x y x' y' Hx Hx' H. rewrite Nat.mul_comm, (Nat.mul_comm y') in H. split. erewrite Nat.div_unique. 3: eassumption. 2: assumption. rewrite H. eapply Nat.div_unique. 2: symmetry; eassumption. assumption. erewrite Nat.mod_unique. 3: eassumption. 2: assumption. rewrite H. eapply Nat.mod_unique. 2: symmetry; eassumption. assumption. Qed.
imports: Psatz PeanoNat Compare_dec Euclid ordinal