proposition: Lemma zmoddivmin : forall a b n : Z, ZMod a b n <-> ZDivides n (a - b).
proof: Proof. unfold ZMod, Divides in |- *. split. intros. elim H. intros. rewrite H0. unfold Zminus in |- *. rewrite Zplus_assoc_reverse. rewrite Zplus_comm. rewrite Zplus_assoc_reverse. rewrite (Zplus_comm (- b) b). rewrite Zplus_opp_r. rewrite <- Zplus_0_r_reverse. split with x. reflexivity. intros. elim H. intros. split with x. rewrite <- H0. unfold Zminus in |- *. rewrite Zplus_assoc. rewrite Zplus_comm. rewrite Zplus_assoc. rewrite Zplus_opp_l. simpl in |- *. reflexivity. Qed.
imports: ZArith lemmas natZ exp divides