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