proposition: Lemma Zdiv_quotient_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 -> q1 = q2.
proof: Proof. intros a b q1 r1 q2 r2 Hq1 Hr1 Hq2 Hr2. assert (Hr : r1 = r2). apply (Zdiv_remainder_unique a b q1 r1 q2 r2); assumption. rewrite Hr in Hq1. rewrite Hq1 in Hq2. assert (Hb0 : b <> 0%Z). assert (Hbpos : (0 < b)%Z). apply (Z.le_lt_trans 0 r1 b). tauto. tauto. auto with zarith. assert (Hb : (q1 * b)%Z = (q2 * b)%Z). auto with zarith. apply (Zmult_intro_rht _ _ _ Hb0 Hb). Qed.
imports: CoRN.model.Zmod.ZBasics