proposition: Lemma mod_plus_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. split with (x + x0)%Z. rewrite H1. rewrite H2. rewrite (Zplus_assoc (b + Z_of_nat n * x0) d (Z_of_nat n * x)). rewrite (Zplus_assoc_reverse b (Z_of_nat n * x0) d). rewrite (Zplus_comm (Z_of_nat n * x0) d). rewrite (Zplus_comm x x0). rewrite (Zmult_plus_distr_r (Z_of_nat n) x0 x). rewrite Zplus_assoc. rewrite Zplus_assoc. reflexivity. Qed.
imports: ZArith lemmas natZ exp divides