proposition: Theorem Zmult_mod: forall a b n, (a * b) mod n = ((a mod n) * (b mod n)) mod n.
proof: Proof. intros a b n. zero_or_not n. apply Z.mul_mod; auto. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms