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