proposition: Lemma zmod_mult_compat : forall a b c d n : Z, ZMod a b n -> ZMod c d n -> ZMod (a * c) (b * d) n.
proof: Proof. unfold ZMod in |- *. intros. elim H. elim H0. intros. rewrite H1. rewrite H2. split with (x0 * d + x * b + n * x0 * x)%Z. rewrite (Zmult_plus_distr_r (b + n * x0) d (n * x)). rewrite Zmult_plus_distr_l. rewrite Zmult_plus_distr_l. rewrite (Zmult_assoc b n x). rewrite (Zmult_comm b n). rewrite (Zmult_assoc (n * x0) n x). rewrite (Zmult_assoc_reverse n x0 n). rewrite (Zmult_assoc_reverse n (x0 * n) x). rewrite (Zmult_assoc_reverse n b x). rewrite <- (Zmult_plus_distr_r n (b * x) (x0 * n * x)). rewrite (Zplus_assoc_reverse (b * d)). rewrite (Zmult_assoc_reverse n x0 d). rewrite <- (Zmult_plus_distr_r n (x0 * d) (b * x + x0 * n * x)). rewrite (Zmult_comm x0 n). rewrite Zplus_assoc. rewrite (Zmult_comm b x). reflexivity. Qed.
imports: ZArith lemmas natZ exp divides