proposition: Lemma divzdiv : forall a b : Z, Divides (Z.abs_nat a) (Z.abs_nat b) -> ZDivides a b.
proof: Proof. intros. elim H. intros d Hd. elim (Zle_or_lt 0 a). elim (Zle_or_lt 0 b). intros. exists (Z_of_nat d). rewrite <- (inj_abs_pos b). rewrite <- (inj_abs_pos a). rewrite <- Znat.inj_mult. rewrite Hd. reflexivity. apply Z.le_ge. assumption. apply Z.le_ge. assumption. intros. exists (- Z_of_nat d)%Z. rewrite <- (Z.opp_involutive b). rewrite <- (inj_abs_neg b). rewrite <- (inj_abs_pos a). rewrite Zmult_comm. rewrite Zopp_mult_distr_l_reverse. rewrite Zmult_comm. rewrite <- Znat.inj_mult. apply (f_equal (A:=Z)). rewrite Hd. reflexivity. apply Z.le_ge. assumption. assumption. elim (Zle_or_lt 0 b). intros. exists (- Z_of_nat d)%Z. rewrite <- (Z.opp_involutive a). rewrite <- (inj_abs_neg a). rewrite <- (inj_abs_pos b). rewrite Zmult_opp_opp. rewrite <- Znat.inj_mult. rewrite Hd. reflexivity. apply Z.le_ge. assumption. assumption. intros. exists (Z_of_nat d). rewrite <- (Z.opp_involutive b). rewrite <- (Z.opp_involutive a). rewrite <- (inj_abs_neg b). rewrite <- (inj_abs_neg a). rewrite Zopp_mult_distr_l_reverse. rewrite <- Znat.inj_mult. apply (f_equal (A:=Z)). rewrite Hd. reflexivity. assumption. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ dec exp