proposition: Lemma Zmod_mult_compat_l : forall x y z : Z, y%=z -> (x*y) %= (x*z).
proof: Proof. intros x y z [q H]; unfold mod_eq in *. apply Zdivide_intro with (x*q). rewrite <- Zmult_minus_distr_l with z y x. rewrite H. rewrite Zmult_assoc. reflexivity. Qed.
imports: Arith ZArith RelationClasses Type_class_definition Lia ZArith Znumtheory