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