proposition: Theorem Zmod_unique_full: forall a b q r, Remainder r b -> a = b*q + r -> r = a mod b.
proof: Proof. Proof Z.mod_unique. Theorem Zmod_unique: forall a b q r, 0 <= r < b -> a = b*q + r -> r = a mod b. Proof. intros; eapply Zmod_unique_full; eauto. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms