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