proposition: Theorem Zdiv_mod_unique_2 : forall b q1 q2 r1 r2:Z, Remainder r1 b -> Remainder r2 b -> b*q1+r1 = b*q2+r2 -> q1=q2 /\ r1=r2.
proof: Proof. Proof Z.div_mod_unique. Theorem Zdiv_unique_full: forall a b q r, Remainder r b -> a = b*q + r -> q = a/b. Proof Z.div_unique. Theorem Zdiv_unique: forall a b q r, 0 <= r < b -> a = b*q + r -> q = a/b. Proof. intros; eapply Zdiv_unique_full; eauto. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms