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