proposition: Lemma Zdiv_remainder_unique : forall a b q1 r1 q2 r2 : Z, a = (q1 * b + r1)%Z -> (0 <= r1 < b)%Z -> a = (q2 * b + r2)%Z -> (0 <= r2 < b)%Z -> r1 = r2.
proof: Proof. intros a b q1 r1 q2 r2 Hq1 Hr1 Hq2 Hr2. apply (Zmodeq_small r1 r2 b). assumption. assumption. assert ((r1 - r2)%Z = ((q2 - q1) * b)%Z). rewrite Hq1 in Hq2. rewrite BinInt.Zmult_minus_distr_r. auto with zarith. rewrite H. apply Zdivides_mult_elim_lft. apply Zdivides_ref. Qed.
imports: CoRN.model.Zmod.ZBasics