proposition: Lemma Zmult_mod_distr_r: forall a b c, (a*c) mod (b*c) = (a mod b) * c.
proof: Proof. intros a b c. zero_or_not b. rewrite (Z.mul_comm b c); zero_or_not c. + now rewrite !Z.mul_0_r. + rewrite (Z.mul_comm c b). apply Z.mul_mod_distr_r; auto. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms