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