proposition: Lemma moddivmin : forall (a b : Z) (n : nat), Mod a b n <-> Divides n (Z.abs_nat (a - b)).
proof: Proof. unfold Mod, 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 (Z.abs_nat x). pattern n at 2 in |- *. rewrite <- (abs_inj n). apply abs_mult. intros. elim H. intros. elim (Zle_or_lt b a). split with (Z_of_nat x). rewrite <- Znat.inj_mult. rewrite <- H0. rewrite inj_abs_pos. unfold Zminus in |- *. rewrite Zplus_assoc. rewrite Zplus_comm. rewrite Zplus_assoc. rewrite Zplus_opp_l. simpl in |- *. reflexivity. apply Z.le_ge. replace 0%Z with (b - b)%Z. unfold Zminus in |- *. apply Zplus_le_compat_r. assumption. unfold Zminus in |- *. apply Zplus_opp_r. split with (- Z_of_nat x)%Z. rewrite Zmult_comm. rewrite Zopp_mult_distr_l_reverse. rewrite <- Znat.inj_mult. rewrite mult_comm. rewrite <- H0. rewrite inj_abs_neg. rewrite Z.opp_involutive. unfold Zminus in |- *. rewrite (Zplus_comm a). rewrite Zplus_assoc. rewrite Zplus_opp_r. simpl in |- *. reflexivity. replace 0%Z with (b - b)%Z. unfold Zminus in |- *. rewrite (Zplus_comm a). rewrite (Zplus_comm b). apply Zplus_lt_compat_l. assumption. unfold Zminus in |- *. apply Zplus_opp_r. Qed.
imports: ZArith lemmas natZ exp divides