proposition: Lemma Zmult_mod_idemp_l: forall a b n, (a mod n * b) mod n = (a * b) mod n.
proof: Proof. intros; rewrite Zmult_mod, Zmod_mod, <- Zmult_mod; auto. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms