proposition: Lemma mod_trans : forall (a b c : Z) (n : nat), Mod a b n -> Mod b c n -> Mod a c n.
proof: Proof. unfold Mod 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 (Z_of_nat n * x) (Z_of_nat n * x0)). reflexivity. Qed.
imports: ZArith lemmas natZ exp divides