proposition: Theorem ZquotientProp : forall m n : Z, n <> 0%Z -> ex (fun r : Z => m = (Zquotient m n * n + r)%Z /\ (Z.abs (Zquotient m n * n) <= Z.abs m)%Z /\ (Z.abs r < Z.abs n)%Z).
proof: Proof. intros m n; unfold Zquotient in |- *; case n; simpl in |- *. intros H; case H; auto. intros n' Hn'; case m; simpl in |- *; auto. exists 0%Z; repeat split; simpl in |- *; auto with zarith. intros m'; generalize (Pdiv_correct m' n'); case (Pdiv m' n'); simpl in |- *; auto. intros q r (H1, H2); exists (oZ1 r); repeat (split; auto with zarith). rewrite <- (inject_nat_convert (Zpos m') m'); auto. rewrite H1. rewrite inj_plus; rewrite inj_mult. rewrite <- (inject_nat_convert (Zpos n') n'); auto. repeat rewrite inj_oZ1; auto. rewrite inj_oZ1; rewrite Z.abs_eq by auto with zarith; lia. rewrite inj_oZ1; rewrite Z.abs_eq; lia. rewrite <- (inject_nat_convert (Zpos n') n'); auto with zarith. intros m'; generalize (Pdiv_correct m' n'); case (Pdiv m' n'); simpl in |- *; auto. intros q r (H1, H2); exists (- oZ1 r)%Z; repeat (split; auto with zarith). replace (Zneg m') with (- Zpos m')%Z; [ idtac | simpl in |- *; auto ]. rewrite <- (inject_nat_convert (Zpos m') m'); auto. rewrite H1. rewrite inj_plus; rewrite inj_mult. repeat rewrite inj_oZ1; lia. rewrite <- Zopp_mult_distr_l; rewrite Zabs_Zopp. rewrite inj_oZ1; rewrite Z.abs_eq by auto with zarith; lia. rewrite Zabs_Zopp. rewrite inj_oZ1; rewrite Z.abs_eq; lia. intros n' Hn'; case m; simpl in |- *; auto. exists 0%Z; repeat split; simpl in |- *; auto with zarith. intros m'; generalize (Pdiv_correct m' n'); case (Pdiv m' n'); simpl in |- *; auto. intros q r (H1, H2); exists (oZ1 r); repeat (split; auto with zarith). replace (Zneg n') with (- Zpos n')%Z; [ idtac | simpl in |- *; auto ]. rewrite <- (inject_nat_convert (Zpos m') m'); auto. rewrite H1. rewrite inj_plus; rewrite inj_mult. rewrite <- (inject_nat_convert (Zpos n') n'); auto. repeat rewrite inj_oZ1; lia. replace (Zneg n') with (- Zpos n')%Z; [ idtac | simpl in |- *; auto ]. rewrite Zmult_opp_opp. rewrite inj_oZ1; rewrite Z.abs_eq by auto with zarith; lia. rewrite inj_oZ1; rewrite Z.abs_eq; lia. rewrite <- (inject_nat_convert (Zpos n') n'); auto with zarith. intros m'; generalize (Pdiv_correct m' n'); case (Pdiv m' n'); simpl in |- *; auto. intros q r (H1, H2); exists (- oZ1 r)%Z; repeat (split; auto with zarith). replace (Zneg m') with (- Zpos m')%Z; [ idtac | simpl in |- *; auto ]. rewrite <- (inject_nat_convert (Zpos m') m'); auto. replace (Zneg n') with (- Zpos n')%Z; [ idtac | simpl in |- *; auto ]. rewrite H1. rewrite inj_plus; rewrite inj_mult. rewrite <- (inject_nat_convert (Zpos n') n'); auto. repeat rewrite inj_oZ1; lia. replace (Zneg n') with (- Zpos n')%Z; [ idtac | simpl in |- *; auto ]. rewrite <- Zopp_mult_distr_r; rewrite Zabs_Zopp. rewrite inj_oZ1; rewrite Z.abs_eq by auto with zarith; lia. rewrite Zabs_Zopp. rewrite inj_oZ1; rewrite Z.abs_eq; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz