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