proposition: Theorem zdiv_rem : forall d n : Z, (d > 0)%Z -> exists q : Z, (exists r : Z, (0 <= r < d)%Z /\ n = (q * d + r)%Z).
proof: Proof. intros d n. intro. elim (Zle_or_lt 0 n). intro. rewrite <- (inj_abs_pos d). rewrite <- (inj_abs_pos n). elim (div_rem (Z.abs_nat d) (Z.abs_nat n)). intro qn. intros. elim H1. intro rn. intros. elim H2. intros. elim H4. intros. split with (Z_of_nat qn). split with (Z_of_nat rn). split. split. change (Z_of_nat 0 <= Z_of_nat rn)%Z in |- *. apply Znat.inj_le. apply le_O_n. apply Znat.inj_lt. assumption. rewrite <- Znat.inj_mult. rewrite <- Znat.inj_plus. apply Znat.inj_eq. assumption. change (Z.abs_nat d > Z.abs_nat 0) in |- *. apply gtzgt. apply Zlt_le_weak. apply Z.gt_lt. assumption. apply Zeq_le. reflexivity. assumption. apply Z.le_ge. assumption. apply Z.le_ge. apply Zlt_le_weak. apply Z.gt_lt. assumption. intro. rewrite <- (inj_abs_pos d). replace n with (- - n)%Z. rewrite <- (inj_abs_neg n). elim (div_rem (Z.abs_nat d) (Z.abs_nat n)). intro qn. intros. elim H1. intro rn. intros. elim H2. intros. elim H4. intros. elim (le_lt_or_eq 0 rn). intro. split with (- Z_of_nat (S qn))%Z. split with (d - Z_of_nat rn)%Z. split. split. rewrite <- (inj_abs_pos d). apply Zle_minus. apply Znat.inj_le. apply lt_le_weak. assumption. apply Z.le_ge. apply Zlt_le_weak. apply Z.gt_lt. assumption. rewrite inj_abs_pos. apply Zplus_lt_reg_l with (Z_of_nat rn). unfold Zminus in |- *. rewrite (Zplus_comm d). rewrite (Zplus_assoc (Z_of_nat rn)). rewrite Zplus_opp_r. simpl in |- *. change (0 + d < Z_of_nat rn + d)%Z in |- *. rewrite Zplus_comm. rewrite (Zplus_comm (Z_of_nat rn)). apply Zplus_lt_compat_l. change (Z_of_nat 0 < Z_of_nat rn)%Z in |- *. apply Znat.inj_lt. assumption. apply Z.le_ge. apply Zlt_le_weak. apply Z.gt_lt. assumption. rewrite Znat.inj_S. unfold Z.succ in |- *. rewrite Zopp_mult_distr_l_reverse. rewrite Zmult_plus_distr_l. rewrite <- Znat.inj_mult. rewrite Zmult_1_l. rewrite (inj_abs_pos d). rewrite Zopp_plus_distr. unfold Zminus in |- *. rewrite Zplus_assoc_reverse. rewrite (Zplus_assoc (- d)). rewrite Zplus_opp_l. simpl in |- *. rewrite <- Zopp_plus_distr. rewrite <- Znat.inj_plus. rewrite <- H6. reflexivity. apply Z.le_ge. apply Zlt_le_weak. apply Z.gt_lt. assumption. intro. split with (- Z_of_nat qn)%Z. split with 0%Z. split. split. unfold Z.le in |- *. simpl in |- *. discriminate. apply Z.le_lt_trans with (Z_of_nat rn). change (Z_of_nat 0 <= Z_of_nat rn)%Z in |- *. apply Znat.inj_le. apply le_O_n. apply Znat.inj_lt. assumption. rewrite <- Zplus_0_r_reverse. rewrite inj_abs_neg. rewrite Zopp_mult_distr_l_reverse. rewrite <- Znat.inj_mult. rewrite <- H7 in H6. rewrite <- plus_n_O in H6. rewrite <- H6. rewrite inj_abs_neg. reflexivity. assumption. assumption. assumption. change (Z.abs_nat d > Z.abs_nat 0) in |- *. apply gtzgt. apply Zlt_le_weak. apply Z.gt_lt. assumption. unfold Z.le in |- *. simpl in |- *. discriminate. assumption. assumption. apply Z.opp_involutive. apply Z.le_ge. apply Zlt_le_weak. apply Z.gt_lt. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ dec exp