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