proposition: Lemma zmod_refl : forall a n : Z, ZMod a a n.
proof: Proof. unfold ZMod in |- *. intros. split with 0%Z. rewrite <- Zmult_0_r_reverse. rewrite <- Zplus_0_r_reverse. reflexivity. Qed.
imports: ZArith lemmas natZ exp divides