(****************************************************************************
                                                                             
          IEEE754  :  NDiv                                                     
                                                                             
          Laurent Thery                                                      
                                                                             
  *****************************************************************************
  Definition of the quotient and divisibility for natural and relative numbers*)
Require Export Omega.
Require Export Paux.
 
Definition oZ1 (x : Option positive) :=
  match x with
  | None => 0%Z
  | Some z => Zpos z
  end.
(* We use the  function Pdiv function to build our Zquotient*)
 
Definition Zquotient (n m : Z) :=
  match n, m with
  | Z0, _ => 0%Z
  | _, Z0 => 0%Z
  | Zpos x, Zpos y => match Pdiv x y with
                      | (x, _) => oZ1 x
                      end
  | Zneg x, Zneg y => match Pdiv x y with
                      | (x, _) => oZ1 x
                      end
  | Zpos x, Zneg y => match Pdiv x y with
                      | (x, _) => (- oZ1 x)%Z
                      end
  | Zneg x, Zpos y => match Pdiv x y with
                      | (x, _) => (- oZ1 x)%Z
                      end
  end.
 
Theorem inj_oZ1 : forall z, oZ1 z = Z_of_nat (oZ z).
intros z; case z; simpl in |- *;
 try (intros; apply sym_equal; apply inject_nat_convert; auto); 
 auto.
Qed.
 
Theorem Zero_le_oZ : forall z, 0 <= oZ z.
(* Goal: forall z : Option positive, le O (oZ z) *)
intros z; case z; simpl in |- *; auto with arith.
Qed.
Hint Resolve Zero_le_oZ: arith.
(* It has the required property *)
 
Theorem ZquotientProp :
 forall m n : Z,
 n <> 0%Z ->
 ex
   (fun r : Z =>
    m = (Zquotient m n * n + r)%Z /\
    (Zabs (Zquotient m n * n) <= Zabs m)%Z /\ (Zabs r < Zabs n)%Z).
(* Goal: forall (m n : Z) (_ : not (@eq Z n Z0)), @ex Z (fun r : Z => and (@eq Z m (Z.add (Z.mul (Zquotient m n) n) r)) (and (Z.le (Z.abs (Z.mul (Zquotient m n) n)) (Z.abs m)) (Z.lt (Z.abs r) (Z.abs n)))) *)
intros m n; unfold Zquotient in |- *; case n; simpl in |- *.
(* Goal: forall _ : not (@eq Z Z0 Z0), @ex Z (fun r : Z => and (@eq Z m (Z.add (Z.mul match m with | Z0 => Z0 | Zpos x => Z0 | Zneg x => Z0 end Z0) r)) (and (Z.le (Z.abs (Z.mul match m with | Z0 => Z0 | Zpos x => Z0 | Zneg x => Z0 end Z0)) (Z.abs m)) (Z.lt (Z.abs r) Z0))) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zpos p) Z0)), @ex Z (fun r : Z => and (@eq Z m (Z.add (Z.mul match m with | Z0 => Z0 | Zpos x => let (x0, _) := Pdiv x p in oZ1 x0 | Zneg x => let (x0, _) := Pdiv x p in Z.opp (oZ1 x0) end (Zpos p)) r)) (and (Z.le (Z.abs (Z.mul match m with | Z0 => Z0 | Zpos x => let (x0, _) := Pdiv x p in oZ1 x0 | Zneg x => let (x0, _) := Pdiv x p in Z.opp (oZ1 x0) end (Zpos p))) (Z.abs m)) (Z.lt (Z.abs r) (Zpos p)))) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), @ex Z (fun r : Z => and (@eq Z m (Z.add (Z.mul match m with | Z0 => Z0 | Zpos x => let (x0, _) := Pdiv x p in Z.opp (oZ1 x0) | Zneg x => let (x0, _) := Pdiv x p in oZ1 x0 end (Zneg p)) r)) (and (Z.le (Z.abs (Z.mul match m with | Z0 => Z0 | Zpos x => let (x0, _) := Pdiv x p in Z.opp (oZ1 x0) | Zneg x => let (x0, _) := Pdiv x p in oZ1 x0 end (Zneg p))) (Z.abs m)) (Z.lt (Z.abs r) (Zpos p)))) *)
intros H; case H; auto.
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), @ex Z (fun r : Z => and (@eq Z m (Z.add (Z.mul match m with | Z0 => Z0 | Zpos x => let (x0, _) := Pdiv x p in Z.opp (oZ1 x0) | Zneg x => let (x0, _) := Pdiv x p in oZ1 x0 end (Zneg p)) r)) (and (Z.le (Z.abs (Z.mul match m with | Z0 => Z0 | Zpos x => let (x0, _) := Pdiv x p in Z.opp (oZ1 x0) | Zneg x => let (x0, _) := Pdiv x p in oZ1 x0 end (Zneg p))) (Z.abs m)) (Z.lt (Z.abs r) (Zpos p)))) *)
intros n' Hn'; case m; simpl in |- *; auto.
(* Goal: @ex Z (fun r : Z => and (@eq Z Z0 r) (and (Z.le Z0 Z0) (Z.lt (Z.abs r) (Zpos n')))) *)
(* Goal: forall p : positive, @ex Z (fun r : Z => and (@eq Z (Zpos p) (Z.add (Z.mul (let (x, _) := Pdiv p n' in Z.opp (oZ1 x)) (Zneg n')) r)) (and (Z.le (Z.abs (Z.mul (let (x, _) := Pdiv p n' in Z.opp (oZ1 x)) (Zneg n'))) (Zpos p)) (Z.lt (Z.abs r) (Zpos n')))) *)
(* Goal: forall p : positive, @ex Z (fun r : Z => and (@eq Z (Zneg p) (Z.add (Z.mul (let (x, _) := Pdiv p n' in oZ1 x) (Zneg n')) r)) (and (Z.le (Z.abs (Z.mul (let (x, _) := Pdiv p n' in oZ1 x) (Zneg n'))) (Zpos p)) (Z.lt (Z.abs r) (Zpos n')))) *)
exists 0%Z; repeat split; simpl in |- *; auto with zarith.
intros m'; generalize (Pdiv_correct m' n'); case (Pdiv m' n'); simpl in |- *;
 auto.
(* Goal: forall (o o0 : Option positive) (_ : and (@eq nat (Pos.to_nat m') (Init.Nat.add (Init.Nat.mul (oZ o) (Pos.to_nat n')) (oZ o0))) (lt (oZ o0) (Pos.to_nat n'))), @ex Z (fun r : Z => and (@eq Z (Zpos m') (Z.add (Z.mul (Z.opp (oZ1 o)) (Zneg n')) r)) (and (Z.le (Z.abs (Z.mul (Z.opp (oZ1 o)) (Zneg n'))) (Zpos m')) (Z.lt (Z.abs r) (Zpos n')))) *)
(* Goal: forall p : positive, @ex Z (fun r : Z => and (@eq Z (Zneg p) (Z.add (Z.mul (let (x, _) := Pdiv p n' in oZ1 x) (Zneg n')) r)) (and (Z.le (Z.abs (Z.mul (let (x, _) := Pdiv p n' in oZ1 x) (Zneg n'))) (Zpos p)) (Z.lt (Z.abs r) (Zpos n')))) *)
intros q r (H1, H2); exists (oZ1 r); repeat (split; auto with zarith).
(* Goal: @eq Z (Z.opp (Zpos m')) (Z.add (Z.mul (oZ1 q) (Zneg n')) (Z.opp (oZ1 r))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite <- (inject_nat_convert (Zpos m') m'); auto.
(* Goal: @eq Z (Z.opp (Z.of_nat (Pos.to_nat m'))) (Z.add (Z.mul (oZ1 q) (Z.opp (Zpos n'))) (Z.opp (oZ1 r))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite H1.
(* Goal: @eq Z (Z.opp (Z.of_nat (Init.Nat.add (Init.Nat.mul (oZ q) (Pos.to_nat n')) (oZ r)))) (Z.add (Z.mul (oZ1 q) (Z.opp (Zpos n'))) (Z.opp (oZ1 r))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite inj_plus; rewrite inj_mult.
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r)))) (Z.add (Z.mul (oZ1 q) (Z.opp (Zpos n'))) (Z.opp (oZ1 r))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite <- (inject_nat_convert (Zpos n') n'); auto.
(* Goal: @eq Z (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r))) (Z.add (Z.mul (oZ1 q) (Z.of_nat (Pos.to_nat n'))) (oZ1 r)) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zpos n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (oZ1 r)) (Zpos n') *)
(* Goal: forall p : positive, @ex Z (fun r : Z => and (@eq Z (Zneg p) (Z.add (Z.mul (let (x, _) := Pdiv p n' in Z.opp (oZ1 x)) (Zpos n')) r)) (and (Z.le (Z.abs (Z.mul (let (x, _) := Pdiv p n' in Z.opp (oZ1 x)) (Zpos n'))) (Zpos p)) (Z.lt (Z.abs r) (Zpos n')))) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), @ex Z (fun r : Z => and (@eq Z m (Z.add (Z.mul match m with | Z0 => Z0 | Zpos x => let (x0, _) := Pdiv x p in Z.opp (oZ1 x0) | Zneg x => let (x0, _) := Pdiv x p in oZ1 x0 end (Zneg p)) r)) (and (Z.le (Z.abs (Z.mul match m with | Z0 => Z0 | Zpos x => let (x0, _) := Pdiv x p in Z.opp (oZ1 x0) | Zneg x => let (x0, _) := Pdiv x p in oZ1 x0 end (Zneg p))) (Z.abs m)) (Z.lt (Z.abs r) (Zpos p)))) *)
repeat rewrite inj_oZ1; auto.
(* Goal: Z.lt (Z.abs (oZ1 r)) (Zpos n') *)
rewrite inj_oZ1; rewrite Zabs_eq; auto with zarith.
(* Goal: Z.le (Z.mul (Z.of_nat (oZ q)) (Zpos n')) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite <- (inject_nat_convert (Zpos m') m'); auto with zarith.
(* Goal: Z.lt (Z.of_nat (oZ r)) (Zpos n') *)
rewrite <- (inject_nat_convert (Zpos n') n'); auto with zarith.
(* Goal: Z.lt (Z.abs (oZ1 r)) (Zpos n') *)
rewrite inj_oZ1; rewrite Zabs_eq; auto with zarith.
(* Goal: Z.lt (Z.of_nat (oZ r)) (Zpos n') *)
rewrite <- (inject_nat_convert (Zpos n') n'); auto with zarith.
intros m'; generalize (Pdiv_correct m' n'); case (Pdiv m' n'); simpl in |- *;
 auto.
(* Goal: forall (o o0 : Option positive) (_ : and (@eq nat (Pos.to_nat m') (Init.Nat.add (Init.Nat.mul (oZ o) (Pos.to_nat n')) (oZ o0))) (lt (oZ o0) (Pos.to_nat n'))), @ex Z (fun r : Z => and (@eq Z (Zneg m') (Z.add (Z.mul (oZ1 o) (Zneg n')) r)) (and (Z.le (Z.abs (Z.mul (oZ1 o) (Zneg n'))) (Zpos m')) (Z.lt (Z.abs r) (Zpos n')))) *)
intros q r (H1, H2); exists (- oZ1 r)%Z; repeat (split; auto with zarith).
(* Goal: @eq Z (Zneg m') (Z.add (Z.mul (oZ1 q) (Zneg n')) (Z.opp (oZ1 r))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
replace (Zneg m') with (- Zpos m')%Z; [ idtac | simpl in |- *; auto ].
(* Goal: @eq Z (Z.opp (Zpos m')) (Z.add (Z.mul (oZ1 q) (Zneg n')) (Z.opp (oZ1 r))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite <- (inject_nat_convert (Zpos m') m'); auto.
(* Goal: @eq Z (Z.opp (Z.of_nat (Pos.to_nat m'))) (Z.add (Z.mul (oZ1 q) (Z.opp (Zpos n'))) (Z.opp (oZ1 r))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite H1.
(* Goal: @eq Z (Z.opp (Z.of_nat (Init.Nat.add (Init.Nat.mul (oZ q) (Pos.to_nat n')) (oZ r)))) (Z.add (Z.mul (oZ1 q) (Z.opp (Zpos n'))) (Z.opp (oZ1 r))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite inj_plus; rewrite inj_mult.
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r)))) (Z.add (Z.mul (oZ1 q) (Z.opp (Zpos n'))) (Z.opp (oZ1 r))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite <- (inject_nat_convert (Zpos n') n'); auto.
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r)))) (Z.add (Z.mul (oZ1 q) (Z.opp (Z.of_nat (Pos.to_nat n')))) (Z.opp (oZ1 r))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
repeat rewrite inj_oZ1; auto with zarith.
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r)))) (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.opp (Z.of_nat (Pos.to_nat n')))) (Z.opp (Z.of_nat (oZ r)))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
ring.
(* Goal: Z.le (Z.abs (Z.mul (Z.opp (oZ1 q)) (Zpos n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), @ex Z (fun r : Z => and (@eq Z m (Z.add (Z.mul match m with | Z0 => Z0 | Zpos x => let (x0, _) := Pdiv x p in Z.opp (oZ1 x0) | Zneg x => let (x0, _) := Pdiv x p in oZ1 x0 end (Zneg p)) r)) (and (Z.le (Z.abs (Z.mul match m with | Z0 => Z0 | Zpos x => let (x0, _) := Pdiv x p in Z.opp (oZ1 x0) | Zneg x => let (x0, _) := Pdiv x p in oZ1 x0 end (Zneg p))) (Z.abs m)) (Z.lt (Z.abs r) (Zpos p)))) *)
rewrite <- Zopp_mult_distr_l; rewrite Zabs_Zopp.
(* Goal: Z.lt (Z.abs (oZ1 r)) (Zpos n') *)
rewrite inj_oZ1; rewrite Zabs_eq; auto with zarith.
(* Goal: Z.le (Z.mul (Z.of_nat (oZ q)) (Zpos n')) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite <- (inject_nat_convert (Zpos m') m'); auto with zarith.
(* Goal: Z.lt (Z.of_nat (oZ r)) (Zpos n') *)
rewrite <- (inject_nat_convert (Zpos n') n'); auto with zarith.
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite Zabs_Zopp.
(* Goal: Z.lt (Z.abs (oZ1 r)) (Zpos n') *)
rewrite inj_oZ1; rewrite Zabs_eq; auto with zarith.
(* Goal: Z.lt (Z.of_nat (oZ r)) (Zpos n') *)
rewrite <- (inject_nat_convert (Zpos n') n'); auto with zarith.
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), @ex Z (fun r : Z => and (@eq Z m (Z.add (Z.mul match m with | Z0 => Z0 | Zpos x => let (x0, _) := Pdiv x p in Z.opp (oZ1 x0) | Zneg x => let (x0, _) := Pdiv x p in oZ1 x0 end (Zneg p)) r)) (and (Z.le (Z.abs (Z.mul match m with | Z0 => Z0 | Zpos x => let (x0, _) := Pdiv x p in Z.opp (oZ1 x0) | Zneg x => let (x0, _) := Pdiv x p in oZ1 x0 end (Zneg p))) (Z.abs m)) (Z.lt (Z.abs r) (Zpos p)))) *)
intros n' Hn'; case m; simpl in |- *; auto.
(* Goal: @ex Z (fun r : Z => and (@eq Z Z0 r) (and (Z.le Z0 Z0) (Z.lt (Z.abs r) (Zpos n')))) *)
(* Goal: forall p : positive, @ex Z (fun r : Z => and (@eq Z (Zpos p) (Z.add (Z.mul (let (x, _) := Pdiv p n' in Z.opp (oZ1 x)) (Zneg n')) r)) (and (Z.le (Z.abs (Z.mul (let (x, _) := Pdiv p n' in Z.opp (oZ1 x)) (Zneg n'))) (Zpos p)) (Z.lt (Z.abs r) (Zpos n')))) *)
(* Goal: forall p : positive, @ex Z (fun r : Z => and (@eq Z (Zneg p) (Z.add (Z.mul (let (x, _) := Pdiv p n' in oZ1 x) (Zneg n')) r)) (and (Z.le (Z.abs (Z.mul (let (x, _) := Pdiv p n' in oZ1 x) (Zneg n'))) (Zpos p)) (Z.lt (Z.abs r) (Zpos n')))) *)
exists 0%Z; repeat split; simpl in |- *; auto with zarith.
intros m'; generalize (Pdiv_correct m' n'); case (Pdiv m' n'); simpl in |- *;
 auto.
(* Goal: forall (o o0 : Option positive) (_ : and (@eq nat (Pos.to_nat m') (Init.Nat.add (Init.Nat.mul (oZ o) (Pos.to_nat n')) (oZ o0))) (lt (oZ o0) (Pos.to_nat n'))), @ex Z (fun r : Z => and (@eq Z (Zpos m') (Z.add (Z.mul (Z.opp (oZ1 o)) (Zneg n')) r)) (and (Z.le (Z.abs (Z.mul (Z.opp (oZ1 o)) (Zneg n'))) (Zpos m')) (Z.lt (Z.abs r) (Zpos n')))) *)
(* Goal: forall p : positive, @ex Z (fun r : Z => and (@eq Z (Zneg p) (Z.add (Z.mul (let (x, _) := Pdiv p n' in oZ1 x) (Zneg n')) r)) (and (Z.le (Z.abs (Z.mul (let (x, _) := Pdiv p n' in oZ1 x) (Zneg n'))) (Zpos p)) (Z.lt (Z.abs r) (Zpos n')))) *)
intros q r (H1, H2); exists (oZ1 r); repeat (split; auto with zarith).
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
replace (Zneg n') with (- Zpos n')%Z; [ idtac | simpl in |- *; auto ].
(* Goal: @eq Z (Z.opp (Zpos m')) (Z.add (Z.mul (oZ1 q) (Zneg n')) (Z.opp (oZ1 r))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite <- (inject_nat_convert (Zpos m') m'); auto.
(* Goal: @eq Z (Z.opp (Z.of_nat (Pos.to_nat m'))) (Z.add (Z.mul (oZ1 q) (Z.opp (Zpos n'))) (Z.opp (oZ1 r))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite H1.
(* Goal: @eq Z (Z.opp (Z.of_nat (Init.Nat.add (Init.Nat.mul (oZ q) (Pos.to_nat n')) (oZ r)))) (Z.add (Z.mul (oZ1 q) (Z.opp (Zpos n'))) (Z.opp (oZ1 r))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite inj_plus; rewrite inj_mult.
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r)))) (Z.add (Z.mul (oZ1 q) (Z.opp (Zpos n'))) (Z.opp (oZ1 r))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite <- (inject_nat_convert (Zpos n') n'); auto.
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r)))) (Z.add (Z.mul (oZ1 q) (Z.opp (Z.of_nat (Pos.to_nat n')))) (Z.opp (oZ1 r))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
repeat rewrite inj_oZ1; auto with zarith.
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r)))) (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.opp (Z.of_nat (Pos.to_nat n')))) (Z.opp (Z.of_nat (oZ r)))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
ring.
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
replace (Zneg n') with (- Zpos n')%Z; [ idtac | simpl in |- *; auto ].
(* Goal: Z.le (Z.abs (Z.mul (Z.opp (oZ1 q)) (Z.opp (Zpos n')))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (oZ1 r)) (Zpos n') *)
(* Goal: forall p : positive, @ex Z (fun r : Z => and (@eq Z (Zneg p) (Z.add (Z.mul (let (x, _) := Pdiv p n' in oZ1 x) (Zneg n')) r)) (and (Z.le (Z.abs (Z.mul (let (x, _) := Pdiv p n' in oZ1 x) (Zneg n'))) (Zpos p)) (Z.lt (Z.abs r) (Zpos n')))) *)
rewrite Zmult_opp_opp.
(* Goal: Z.lt (Z.abs (oZ1 r)) (Zpos n') *)
rewrite inj_oZ1; rewrite Zabs_eq; auto with zarith.
(* Goal: Z.lt (Z.of_nat (oZ r)) (Zpos n') *)
rewrite <- (inject_nat_convert (Zpos n') n'); auto with zarith.
(* Goal: Z.le (Z.mul (Z.of_nat (oZ q)) (Zpos n')) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite <- (inject_nat_convert (Zpos m') m'); auto with zarith.
(* Goal: Z.lt (Z.abs (oZ1 r)) (Zpos n') *)
rewrite inj_oZ1; rewrite Zabs_eq; auto with zarith.
(* Goal: Z.lt (Z.of_nat (oZ r)) (Zpos n') *)
rewrite <- (inject_nat_convert (Zpos n') n'); auto with zarith.
intros m'; generalize (Pdiv_correct m' n'); case (Pdiv m' n'); simpl in |- *;
 auto.
(* Goal: forall (o o0 : Option positive) (_ : and (@eq nat (Pos.to_nat m') (Init.Nat.add (Init.Nat.mul (oZ o) (Pos.to_nat n')) (oZ o0))) (lt (oZ o0) (Pos.to_nat n'))), @ex Z (fun r : Z => and (@eq Z (Zneg m') (Z.add (Z.mul (oZ1 o) (Zneg n')) r)) (and (Z.le (Z.abs (Z.mul (oZ1 o) (Zneg n'))) (Zpos m')) (Z.lt (Z.abs r) (Zpos n')))) *)
intros q r (H1, H2); exists (- oZ1 r)%Z; repeat (split; auto with zarith).
(* Goal: @eq Z (Zneg m') (Z.add (Z.mul (oZ1 q) (Zneg n')) (Z.opp (oZ1 r))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
replace (Zneg m') with (- Zpos m')%Z; [ idtac | simpl in |- *; auto ].
(* Goal: @eq Z (Z.opp (Zpos m')) (Z.add (Z.mul (oZ1 q) (Zneg n')) (Z.opp (oZ1 r))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite <- (inject_nat_convert (Zpos m') m'); auto.
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
replace (Zneg n') with (- Zpos n')%Z; [ idtac | simpl in |- *; auto ].
(* Goal: @eq Z (Z.opp (Z.of_nat (Pos.to_nat m'))) (Z.add (Z.mul (oZ1 q) (Z.opp (Zpos n'))) (Z.opp (oZ1 r))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite H1.
(* Goal: @eq Z (Z.opp (Z.of_nat (Init.Nat.add (Init.Nat.mul (oZ q) (Pos.to_nat n')) (oZ r)))) (Z.add (Z.mul (oZ1 q) (Z.opp (Zpos n'))) (Z.opp (oZ1 r))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite inj_plus; rewrite inj_mult.
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r)))) (Z.add (Z.mul (oZ1 q) (Z.opp (Zpos n'))) (Z.opp (oZ1 r))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite <- (inject_nat_convert (Zpos n') n'); auto.
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r)))) (Z.add (Z.mul (oZ1 q) (Z.opp (Z.of_nat (Pos.to_nat n')))) (Z.opp (oZ1 r))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
repeat rewrite inj_oZ1; auto with zarith.
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r)))) (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.opp (Z.of_nat (Pos.to_nat n')))) (Z.opp (Z.of_nat (oZ r)))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
ring.
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
replace (Zneg n') with (- Zpos n')%Z; [ idtac | simpl in |- *; auto ].
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite <- Zopp_mult_distr_r; rewrite Zabs_Zopp.
(* Goal: Z.lt (Z.abs (oZ1 r)) (Zpos n') *)
rewrite inj_oZ1; rewrite Zabs_eq; auto with zarith.
(* Goal: Z.le (Z.mul (Z.of_nat (oZ q)) (Zpos n')) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite <- (inject_nat_convert (Zpos m') m'); auto with zarith.
(* Goal: Z.lt (Z.of_nat (oZ r)) (Zpos n') *)
rewrite <- (inject_nat_convert (Zpos n') n'); auto with zarith.
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite Zabs_Zopp.
(* Goal: Z.lt (Z.abs (oZ1 r)) (Zpos n') *)
rewrite inj_oZ1; rewrite Zabs_eq; auto with zarith.
(* Goal: Z.lt (Z.of_nat (oZ r)) (Zpos n') *)
rewrite <- (inject_nat_convert (Zpos n') n'); auto with zarith.
Qed.
 
Theorem ZquotientPos :
 forall z1 z2 : Z, (0 <= z1)%Z -> (0 <= z2)%Z -> (0 <= Zquotient z1 z2)%Z.
(* Goal: forall (z1 z2 : Z) (_ : Z.le Z0 z1) (_ : Z.le Z0 z2), Z.le Z0 (Zquotient z1 z2) *)
intros z1 z2 H H0; case (Z_eq_dec z2 0); intros Z1.
rewrite Z1; red in |- *; case z1; simpl in |- *; auto; intros; red in |- *;
 intros; discriminate.
(* Goal: Z.le Z0 (Zquotient z1 z2) *)
case (ZquotientProp z1 z2); auto; intros r (H1, (H2, H3)).
(* Goal: Z.le Z0 (Zquotient z1 z2) *)
case (Zle_or_lt 0 (Zquotient z1 z2)); auto; intros Z2.
(* Goal: Z.le Z0 (Zquotient z1 z2) *)
Contradict H3; apply Zle_not_lt.
replace r with (z1 - Zquotient z1 z2 * z2)%Z;
 [ idtac | pattern z1 at 1 in |- *; rewrite H1; ring ].
(* Goal: Z.le (Z.abs z2) (Z.abs (Z.sub z1 (Z.mul (Zquotient z1 z2) z2))) *)
repeat rewrite Zabs_eq; auto.
(* Goal: Z.le z2 (Z.sub z1 (Z.mul (Zquotient z1 z2) z2)) *)
(* Goal: Z.le Z0 (Z.sub z1 (Z.mul (Zquotient z1 z2) z2)) *)
pattern z2 at 1 in |- *; replace z2 with (0 + 1 * z2)%Z; [ idtac | ring ].
(* Goal: Z.le (Z.add Z0 (Z.mul (Zpos xH) z2)) (Z.sub z1 (Z.mul (Zquotient z1 z2) z2)) *)
(* Goal: Z.le Z0 (Z.sub z1 (Z.mul (Zquotient z1 z2) z2)) *)
unfold Zminus in |- *; apply Zle_trans with (z1 + 1 * z2)%Z; auto with zarith.
(* Goal: Z.le (Z.add z1 (Z.mul (Zpos xH) z2)) (Z.add z1 (Z.opp (Z.mul (Zquotient z1 z2) z2))) *)
(* Goal: Z.le Z0 (Z.sub z1 (Z.mul (Zquotient z1 z2) z2)) *)
apply Zplus_le_compat_l.
(* Goal: Z.le (Z.mul (Zpos xH) z2) (Z.opp (Z.mul (Zquotient z1 z2) z2)) *)
(* Goal: Z.le Z0 (Z.sub z1 (Z.mul (Zquotient z1 z2) z2)) *)
rewrite Zopp_mult_distr_l.
(* Goal: Z.le (Z.mul (Zpos xH) z2) (Z.mul (Z.opp (Zquotient z1 z2)) z2) *)
(* Goal: Z.le Z0 (Z.sub z1 (Z.mul (Zquotient z1 z2) z2)) *)
apply Zle_Zmult_comp_r; auto with zarith.
(* Goal: Z.le Z0 (Z.sub z1 (Z.mul (Zquotient z1 z2) z2)) *)
unfold Zminus in |- *; rewrite Zopp_mult_distr_l; auto with zarith.
Qed.
(* The property of a  number to divide another one 
     (Ndivides n m) shoud be read as m divides n *)
 
Definition Zdivides (n m : Z) := exists q : Z, n = (m * q)%Z.
 
Theorem ZdividesZquotient :
 forall n m : Z, m <> 0%Z -> Zdivides n m -> n = (Zquotient n m * m)%Z.
(* Goal: forall (n m : Z) (_ : not (@eq Z m Z0)) (_ : Zdivides n m), @eq Z n (Z.mul (Zquotient n m) m) *)
intros n m H' H'0.
(* Goal: @eq Z n (Z.mul (Zquotient n m) m) *)
case H'0; intros z1 Hz1.
(* Goal: @eq Z n (Z.mul (Zquotient n m) m) *)
case (ZquotientProp n m); auto; intros z2 (Hz2, (Hz3, Hz4)).
cut (z2 = 0%Z);
 [ intros H1; pattern n at 1 in |- *; rewrite Hz2; rewrite H1; ring | idtac ].
(* Goal: @eq Z z2 Z0 *)
cut (z2 = ((z1 - Zquotient n m) * m)%Z); [ intros H2 | idtac ].
(* Goal: @eq Z z2 Z0 *)
(* Goal: @eq Z z2 (Z.mul (Z.sub z1 (Zquotient n m)) m) *)
case (Z_eq_dec (z1 - Zquotient n m) 0); intros H3.
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r)))) (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.opp (Z.of_nat (Pos.to_nat n')))) (Z.opp (Z.of_nat (oZ r)))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite H2; rewrite H3; ring.
(* Goal: @eq Z z2 Z0 *)
(* Goal: @eq Z z2 (Z.mul (Z.sub z1 (Zquotient n m)) m) *)
Contradict Hz4.
(* Goal: not (Z.lt (Z.abs z2) (Z.abs m)) *)
(* Goal: @eq Z z2 (Z.mul (Z.sub z1 (Zquotient n m)) m) *)
replace (Zabs m) with (1 * Zabs m)%Z; [ idtac | ring ].
(* Goal: not (Z.lt (Z.abs z2) (Z.mul (Zpos xH) (Z.abs m))) *)
(* Goal: @eq Z z2 (Z.mul (Z.sub z1 (Zquotient n m)) m) *)
apply Zle_not_lt; rewrite H2.
(* Goal: Z.le (Z.mul (Zpos xH) z2) (Z.mul (Z.opp (Zquotient z1 z2)) z2) *)
(* Goal: Z.le Z0 (Z.sub z1 (Z.mul (Zquotient z1 z2) z2)) *)
rewrite Zabs_Zmult; apply Zle_Zmult_comp_r; auto with zarith.
generalize H3; case (z1 - Zquotient n m)%Z;
 try (intros H1; case H1; auto; fail); simpl in |- *; 
 intros p; case p; simpl in |- *; auto; intros; red in |- *; 
(* Goal: not (@eq Z (Zpos xH) Z0) *)
(* Goal: forall (x : Z) (_ : and (@eq Z m (Z.add (Z.mul (Zquotient m (Zpos xH)) (Zpos xH)) x)) (and (Z.le (Z.abs (Z.mul (Zquotient m (Zpos xH)) (Zpos xH))) (Z.abs m)) (Z.lt (Z.abs x) (Z.abs (Zpos xH))))), @eq Z (Zquotient m (Zpos xH)) m *)
 simpl in |- *; auto; red in |- *; intros; discriminate.
rewrite Zmult_minus_distr_r; rewrite (Zmult_comm z1); rewrite <- Hz1;
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r)))) (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.opp (Z.of_nat (Pos.to_nat n')))) (Z.opp (Z.of_nat (oZ r)))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
 (pattern n at 1 in |- *; rewrite Hz2); ring.
Qed.
 
Theorem ZdividesZquotientInv :
 forall n m : Z, n = (Zquotient n m * m)%Z -> Zdivides n m.
(* Goal: forall (n m : Z) (_ : @eq Z n (Z.mul (Zquotient n m) m)), Zdivides n m *)
intros n m H'; red in |- *.
(* Goal: @ex Z (fun q : Z => @eq Z n (Z.mul m q)) *)
exists (Zquotient n m); auto.
(* Goal: @eq Z n (Z.mul m (Zquotient n m)) *)
pattern n at 1 in |- *; rewrite H'; auto with zarith.
Qed.
 
Theorem ZdividesMult :
 forall n m p : Z, Zdivides n m -> Zdivides (p * n) (p * m).
(* Goal: forall (n m p : Z) (_ : Zdivides n m), Zdivides (Z.mul p n) (Z.mul p m) *)
intros n m p H'; red in H'.
(* Goal: Zdivides (Z.mul p n) (Z.mul p m) *)
elim H'; intros q E.
(* Goal: Zdivides (Z.mul p n) (Z.mul p m) *)
red in |- *.
(* Goal: Zdivides n m *)
exists q.
(* Goal: @eq Z (Z.mul p n) (Z.mul (Z.mul p m) q) *)
rewrite E.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
auto with zarith.
Qed.
 
Theorem Zeq_mult_simpl :
 forall a b c : Z, c <> 0%Z -> (a * c)%Z = (b * c)%Z -> a = b.
(* Goal: forall (a b c : Z) (_ : not (@eq Z c Z0)) (_ : @eq Z (Z.mul a c) (Z.mul b c)), @eq Z a b *)
intros a b c H H0.
(* Goal: @eq Z a b *)
case (Zle_or_lt c 0); intros Zl1.
apply Zle_antisym; apply Zmult_le_reg_r with (p := (- c)%Z); try apply Zlt_gt;
 auto with zarith; repeat rewrite <- Zopp_mult_distr_r; 
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
 rewrite H0; auto with zarith.
apply Zle_antisym; apply Zmult_le_reg_r with (p := c); try apply Zlt_gt;
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
 auto with zarith; rewrite H0; auto with zarith.
Qed.
 
Theorem ZdividesDiv :
 forall n m p : Z, p <> 0%Z -> Zdivides (p * n) (p * m) -> Zdivides n m.
(* Goal: forall (n m p : Z) (_ : Zdivides n m) (_ : Zdivides m p), Zdivides n p *)
intros n m p H' H'0.
(* Goal: Zdivides n m *)
case H'0; intros q E.
(* Goal: Zdivides n m *)
exists q.
(* Goal: @eq Z n (Z.mul m q) *)
apply Zeq_mult_simpl with (c := p); auto.
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r)))) (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.opp (Z.of_nat (Pos.to_nat n')))) (Z.opp (Z.of_nat (oZ r)))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
rewrite (Zmult_comm n); rewrite E; ring.
Qed.
 
Definition ZdividesP : forall n m : Z, {Zdivides n m} + {~ Zdivides n m}.
(* Goal: forall n m : Z, sumbool (Zdivides n m) (not (Zdivides n m)) *)
intros n m; case m.
(* Goal: sumbool (Zdivides n Z0) (not (Zdivides n Z0)) *)
(* Goal: forall p : positive, sumbool (Zdivides n (Zpos p)) (not (Zdivides n (Zpos p))) *)
(* Goal: forall p : positive, sumbool (Zdivides n (Zneg p)) (not (Zdivides n (Zneg p))) *)
case n.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
left; red in |- *; exists 0%Z; auto with zarith.
intros p; right; red in |- *; intros H; case H; simpl in |- *; intros f H1;
 discriminate.
intros p; right; red in |- *; intros H; case H; simpl in |- *; intros f H1;
 discriminate.
intros p; generalize (Z_eq_bool_correct (Zquotient n (Zpos p) * Zpos p) n);
 case (Z_eq_bool (Zquotient n (Zpos p) * Zpos p) n); 
 intros H1.
(* Goal: sumbool (Zdivides n (Zneg p)) (not (Zdivides n (Zneg p))) *)
(* Goal: sumbool (Zdivides n (Zneg p)) (not (Zdivides n (Zneg p))) *)
left; apply ZdividesZquotientInv; auto.
(* Goal: sumbool (Zdivides n (Zneg p)) (not (Zdivides n (Zneg p))) *)
right; Contradict H1; apply sym_equal; apply ZdividesZquotient; auto.
(* Goal: not (@eq Z (Zpos xH) Z0) *)
(* Goal: forall (x : Z) (_ : and (@eq Z m (Z.add (Z.mul (Zquotient m (Zpos xH)) (Zpos xH)) x)) (and (Z.le (Z.abs (Z.mul (Zquotient m (Zpos xH)) (Zpos xH))) (Z.abs m)) (Z.lt (Z.abs x) (Z.abs (Zpos xH))))), @eq Z (Zquotient m (Zpos xH)) m *)
red in |- *; intros; discriminate.
intros p; generalize (Z_eq_bool_correct (Zquotient n (Zneg p) * Zneg p) n);
 case (Z_eq_bool (Zquotient n (Zneg p) * Zneg p) n); 
 intros H1.
(* Goal: sumbool (Zdivides n (Zneg p)) (not (Zdivides n (Zneg p))) *)
(* Goal: sumbool (Zdivides n (Zneg p)) (not (Zdivides n (Zneg p))) *)
left; apply ZdividesZquotientInv; auto.
(* Goal: sumbool (Zdivides n (Zneg p)) (not (Zdivides n (Zneg p))) *)
right; Contradict H1; apply sym_equal; apply ZdividesZquotient; auto.
(* Goal: not (@eq Z (Zpos xH) Z0) *)
(* Goal: forall (x : Z) (_ : and (@eq Z m (Z.add (Z.mul (Zquotient m (Zpos xH)) (Zpos xH)) x)) (and (Z.le (Z.abs (Z.mul (Zquotient m (Zpos xH)) (Zpos xH))) (Z.abs m)) (Z.lt (Z.abs x) (Z.abs (Zpos xH))))), @eq Z (Zquotient m (Zpos xH)) m *)
red in |- *; intros; discriminate.
Defined.
(* Eval Compute in (ZdividesP (POS (xO (xO xH))) (POS (xO xH))). *)
 
Theorem Zquotient1 : forall m : Z, Zquotient m 1 = m.
(* Goal: forall m : Z, @eq Z (Zquotient m (Zpos xH)) m *)
intros m.
(* Goal: @eq Z (Zquotient m (Zpos xH)) m *)
case (ZquotientProp m 1); auto.
(* Goal: not (@eq Z (Zpos xH) Z0) *)
(* Goal: forall (x : Z) (_ : and (@eq Z m (Z.add (Z.mul (Zquotient m (Zpos xH)) (Zpos xH)) x)) (and (Z.le (Z.abs (Z.mul (Zquotient m (Zpos xH)) (Zpos xH))) (Z.abs m)) (Z.lt (Z.abs x) (Z.abs (Zpos xH))))), @eq Z (Zquotient m (Zpos xH)) m *)
red in |- *; intros; discriminate.
(* Goal: forall (x : Z) (_ : and (@eq Z m (Z.add (Z.mul (Zquotient m (Zpos xH)) (Zpos xH)) x)) (and (Z.le (Z.abs (Z.mul (Zquotient m (Zpos xH)) (Zpos xH))) (Z.abs m)) (Z.lt (Z.abs x) (Z.abs (Zpos xH))))), @eq Z (Zquotient m (Zpos xH)) m *)
intros z (H1, (H2, H3)).
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r)))) (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.opp (Z.of_nat (Pos.to_nat n')))) (Z.opp (Z.of_nat (oZ r)))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
pattern m at 2 in |- *; rewrite H1; replace z with 0%Z; try ring.
generalize H3; case z; simpl in |- *; auto; intros p; case p;
 unfold Zlt in |- *; simpl in |- *; intros; discriminate.
Qed.
 
Theorem Zdivides1 : forall m : Z, Zdivides m 1.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
intros m; exists m; auto with zarith.
Qed.
 
Theorem Zabs_eq_case :
 forall z1 z2 : Z, Zabs z1 = Zabs z2 -> z1 = z2 \/ z1 = (- z2)%Z.
intros z1 z2; case z1; case z2; simpl in |- *; auto;
 try (intros; discriminate); intros p1 p2 H1; injection H1;
 (intros H2; rewrite H2); auto.
Qed.
 
Theorem Zabs_tri : forall z1 z2 : Z, (Zabs (z1 + z2) <= Zabs z1 + Zabs z2)%Z.
(* Goal: forall z1 z2 : Z, Z.le (Z.abs (Z.add z1 z2)) (Z.add (Z.abs z1) (Z.abs z2)) *)
intros z1 z2; case z1; case z2; try (simpl in |- *; auto with zarith; fail).
intros p1 p2;
 apply
  Zabs_intro with (P := fun x => (x <= Zabs (Zpos p2) + Zabs (Zneg p1))%Z);
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
 try rewrite Zopp_plus_distr; auto with zarith.
intros p1 p2;
 apply
  Zabs_intro with (P := fun x => (x <= Zabs (Zpos p2) + Zabs (Zneg p1))%Z);
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
 try rewrite Zopp_plus_distr; auto with zarith.
Qed.
Hint Resolve Zabs_tri: zarith.
 
Theorem ZquotientUnique :
 forall m n q r : Z,
 n <> 0%Z ->
 m = (q * n + r)%Z ->
 (Zabs (q * n) <= Zabs m)%Z -> (Zabs r < Zabs n)%Z -> q = Zquotient m n.
(* Goal: forall (m n q r : Z) (_ : not (@eq Z n Z0)) (_ : @eq Z m (Z.add (Z.mul q n) r)) (_ : Z.le (Z.abs (Z.mul q n)) (Z.abs m)) (_ : Z.lt (Z.abs r) (Z.abs n)), @eq Z q (Zquotient m n) *)
intros m n q r H' H'0 H'1 H'2.
(* Goal: @eq Z q (Zquotient m n) *)
case (ZquotientProp m n); auto; intros z (H0, (H1, H2)).
(* Goal: @eq Z q (Zquotient m n) *)
case (Zle_or_lt (Zabs q) (Zabs (Zquotient m n))); intros Zl1; auto with arith.
(* Goal: @eq Z q (Zquotient m n) *)
(* Goal: @eq Z q (Zquotient m n) *)
case (Zle_lt_or_eq _ _ Zl1); clear Zl1; intros Zl1; auto with arith.
(* Goal: @eq Z q (Zquotient m n) *)
(* Goal: @eq Z q (Zquotient m n) *)
(* Goal: @eq Z q (Zquotient m n) *)
Contradict H1; apply Zlt_not_le.
(* Goal: Z.lt (Z.abs m) (Z.abs (Z.mul (Zquotient m n) n)) *)
(* Goal: @eq Z q (Zquotient m n) *)
(* Goal: @eq Z q (Zquotient m n) *)
pattern m at 1 in |- *; rewrite H'0.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
apply Zle_lt_trans with (Zabs (q * n) + Zabs r)%Z; auto with zarith.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
apply Zlt_le_trans with (Zabs (q * n) + Zabs n)%Z; auto with zarith.
(* Goal: Z.le (Z.add (Z.abs (Z.mul (Zquotient m q) q)) (Z.abs q)) (Z.abs (Z.mul (Zquotient n q) q)) *)
(* Goal: Z.le (Z.abs (Zquotient n q)) (Z.abs (Zquotient m q)) *)
repeat rewrite Zabs_Zmult.
replace (Zabs q * Zabs n + Zabs n)%Z with (Zsucc (Zabs q) * Zabs n)%Z;
 [ auto with zarith | unfold Zsucc in |- *; ring ].
(* Goal: @eq Z q (Zquotient m n) *)
(* Goal: @eq Z q (Zquotient m n) *)
case (Zabs_eq_case _ _ Zl1); auto.
intros H;
 (cut (Zquotient m n = 0%Z);
   [ intros H3; rewrite H; repeat rewrite H3; simpl in |- *; auto | idtac ]).
(* Goal: @eq Z (Zquotient m n) Z0 *)
(* Goal: @eq Z q (Zquotient m n) *)
cut (Zabs (Zquotient m n) < 1)%Z.
case (Zquotient m n); simpl in |- *; auto; intros p; case p;
 unfold Zlt in |- *; simpl in |- *; intros; discriminate.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
apply Zlt_mult_simpl_l with (c := Zabs n); auto with zarith.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
case (Zle_lt_or_eq 0 (Zabs n)); auto with zarith.
(* Goal: forall _ : @eq Z Z0 (Z.abs n), Z.lt Z0 (Z.abs n) *)
(* Goal: Z.lt (Z.mul (Z.abs n) (Z.abs (Zquotient m n))) (Z.mul (Z.abs n) (Zpos xH)) *)
(* Goal: @eq Z q (Zquotient m n) *)
intros H3; case H'; auto.
(* Goal: @eq Z n Z0 *)
(* Goal: Z.lt (Z.mul (Z.abs n) (Z.abs (Zquotient m n))) (Z.mul (Z.abs n) (Zpos xH)) *)
(* Goal: @eq Z q (Zquotient m n) *)
generalize H3; case n; simpl in |- *; auto; intros; discriminate.
(* Goal: Z.lt (Z.mul (Z.abs n) (Z.abs (Zquotient m n))) (Z.mul (Z.abs n) (Zpos xH)) *)
(* Goal: @eq Z q (Zquotient m n) *)
rewrite <- Zabs_Zmult; rewrite (Zmult_comm n).
(* Goal: Z.lt (Z.abs (Z.mul (Zquotient m n) n)) (Z.mul (Z.abs n) (Zpos xH)) *)
(* Goal: @eq Z q (Zquotient m n) *)
replace (Zabs n * 1)%Z with (Zabs n); [ idtac | ring ].
(* Goal: Z.lt (Z.abs (Z.mul (Zquotient m n) n)) (Z.abs n) *)
(* Goal: @eq Z q (Zquotient m n) *)
apply Zle_lt_trans with (1 := H1).
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
apply Zlt_mult_simpl_l with (c := (1 + 1)%Z); auto with zarith.
(* Goal: Z.lt (Z.mul (Z.add (Zpos xH) (Zpos xH)) (Z.abs m)) (Z.mul (Z.add (Zpos xH) (Zpos xH)) (Z.abs n)) *)
(* Goal: @eq Z q (Zquotient m n) *)
replace ((1 + 1) * Zabs m)%Z with (Zabs (m + m)).
(* Goal: Z.lt (Z.abs (Z.add m m)) (Z.mul (Z.add (Zpos xH) (Zpos xH)) (Z.abs n)) *)
(* Goal: @eq Z (Z.abs (Z.add m m)) (Z.mul (Z.add (Zpos xH) (Zpos xH)) (Z.abs m)) *)
(* Goal: @eq Z q (Zquotient m n) *)
replace ((1 + 1) * Zabs n)%Z with (Zabs n + Zabs n)%Z; [ idtac | ring ].
(* Goal: Z.lt (Z.abs (Z.add m m)) (Z.add (Z.abs n) (Z.abs n)) *)
(* Goal: @eq Z (Z.abs (Z.add m m)) (Z.mul (Z.add (Zpos xH) (Zpos xH)) (Z.abs m)) *)
(* Goal: @eq Z q (Zquotient m n) *)
pattern m at 1 in |- *; rewrite H'0; rewrite H0; rewrite H.
replace (- Zquotient m n * n + r + (Zquotient m n * n + z))%Z with (r + z)%Z;
 [ idtac | ring ].
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
apply Zle_lt_trans with (Zabs r + Zabs z)%Z; auto with zarith.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
rewrite <- (Zabs_eq (1 + 1)); auto with zarith.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
rewrite <- Zabs_Zmult; apply f_equal with (f := Zabs); auto with zarith.
(* Goal: @eq Z q (Zquotient m n) *)
Contradict H'1; apply Zlt_not_le.
(* Goal: Z.lt (Z.abs m) (Z.abs (Z.mul q n)) *)
pattern m at 1 in |- *; rewrite H0.
apply Zle_lt_trans with (Zabs (Zquotient m n * n) + Zabs z)%Z;
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
 auto with zarith.
apply Zlt_le_trans with (Zabs (Zquotient m n * n) + Zabs n)%Z;
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
 auto with zarith.
(* Goal: Z.le (Z.add (Z.abs (Z.mul (Zquotient m q) q)) (Z.abs q)) (Z.abs (Z.mul (Zquotient n q) q)) *)
(* Goal: Z.le (Z.abs (Zquotient n q)) (Z.abs (Zquotient m q)) *)
repeat rewrite Zabs_Zmult.
replace (Zabs (Zquotient m n) * Zabs n + Zabs n)%Z with
 (Zsucc (Zabs (Zquotient m n)) * Zabs n)%Z;
 [ auto with zarith | unfold Zsucc in |- *; ring ].
Qed.
 
Theorem ZquotientZopp :
 forall m n : Z, Zquotient (- m) n = (- Zquotient m n)%Z.
(* Goal: forall m n : Z, @eq Z (Zquotient (Z.opp m) n) (Z.opp (Zquotient m n)) *)
intros m n; case (Z_eq_dec n 0); intros Z1.
(* Goal: @eq Z (Zquotient (Z.opp m) n) (Z.opp (Zquotient m n)) *)
(* Goal: @eq Z (Zquotient (Z.opp m) n) (Z.opp (Zquotient m n)) *)
rewrite Z1; unfold Zquotient in |- *; case n; case m; simpl in |- *; auto.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
case (ZquotientProp m n); auto; intros r1 (H'2, (H'3, H'4)); auto with zarith.
apply sym_equal;
 apply ZquotientUnique with (q := (- Zquotient m n)%Z) (r := (- r1)%Z); 
 auto.
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r)))) (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.opp (Z.of_nat (Pos.to_nat n')))) (Z.opp (Z.of_nat (oZ r)))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
pattern m at 1 in |- *; rewrite H'2; ring.
(* Goal: Z.le (Z.abs (Z.mul (Z.opp (Zquotient m n)) n)) (Z.abs (Z.opp m)) *)
(* Goal: Z.lt (Z.abs (Z.opp r1)) (Z.abs n) *)
rewrite <- Zopp_mult_distr_l; repeat rewrite Zabs_Zopp; auto.
(* Goal: Z.lt (Z.abs (Z.opp r1)) (Z.abs n) *)
rewrite Zabs_Zopp; auto.
Qed.
 
Theorem ZquotientMonotone :
 forall n m q : Z,
 (Zabs n <= Zabs m)%Z -> (Zabs (Zquotient n q) <= Zabs (Zquotient m q))%Z.
(* Goal: forall (n m q : Z) (_ : Z.le (Z.abs n) (Z.abs m)), Z.le (Z.abs (Zquotient n q)) (Z.abs (Zquotient m q)) *)
intros n m q H; case (Zle_lt_or_eq _ _ H); intros Z0.
(* Goal: Z.le (Zpower_nat r (digit r v)) (Z.abs v) *)
case (Z_eq_dec q 0); intros Z1.
rewrite Z1; unfold Zquotient in |- *; case n; case m; simpl in |- *;
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
 auto with zarith.
case (Zle_or_lt (Zabs (Zquotient n q)) (Zabs (Zquotient m q))); auto;
 intros H'1.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
case (ZquotientProp m q); auto; intros r1 (H'2, (H'3, H'4)); auto with zarith.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
case (ZquotientProp n q); auto; intros r2 (H'5, (H'6, H'7)); auto with zarith.
(* Goal: Z.le (Z.abs (Zquotient n q)) (Z.abs (Zquotient m q)) *)
(* Goal: Z.le (Z.abs (Zquotient n q)) (Z.abs (Zquotient m q)) *)
Contradict H'6.
(* Goal: not (Z.le (Z.abs (Z.mul (Zquotient n q) q)) (Z.abs n)) *)
(* Goal: Z.le (Z.abs (Zquotient n q)) (Z.abs (Zquotient m q)) *)
apply Zlt_not_le.
(* Goal: Z.lt (Z.abs n) (Z.abs (Z.mul (Zquotient n q) q)) *)
(* Goal: Z.le (Z.abs (Zquotient n q)) (Z.abs (Zquotient m q)) *)
apply Zlt_le_trans with (1 := Z0).
(* Goal: Z.le (Z.abs m) (Z.abs (Z.mul (Zquotient n q) q)) *)
(* Goal: Z.le (Z.abs (Zquotient n q)) (Z.abs (Zquotient m q)) *)
rewrite H'2.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
apply Zle_trans with (Zabs (Zquotient m q * q) + Zabs r1)%Z; auto with zarith.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
apply Zle_trans with (Zabs (Zquotient m q * q) + Zabs q)%Z; auto with zarith.
(* Goal: Z.le (Z.add (Z.abs (Z.mul (Zquotient m q) q)) (Z.abs q)) (Z.abs (Z.mul (Zquotient n q) q)) *)
(* Goal: Z.le (Z.abs (Zquotient n q)) (Z.abs (Zquotient m q)) *)
repeat rewrite Zabs_Zmult.
replace (Zabs (Zquotient m q) * Zabs q + Zabs q)%Z with
 (Zsucc (Zabs (Zquotient m q)) * Zabs q)%Z;
 [ idtac | unfold Zsucc in |- *; ring ].
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
cut (0 < Zabs q)%Z; auto with zarith.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
case (Zle_lt_or_eq 0 (Zabs q)); auto with zarith.
(* Goal: forall _ : @eq Z BinNums.Z0 (Z.abs q), Z.lt BinNums.Z0 (Z.abs q) *)
(* Goal: Z.le (Z.abs (Zquotient n q)) (Z.abs (Zquotient m q)) *)
intros H'6; case Z1; auto.
(* Goal: @eq Z q BinNums.Z0 *)
(* Goal: Z.le (Z.abs (Zquotient n q)) (Z.abs (Zquotient m q)) *)
generalize H'6; case q; simpl in |- *; auto; intros; discriminate.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
case (Zabs_eq_case _ _ Z0); intros Z1; rewrite Z1; auto with zarith.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
rewrite ZquotientZopp; rewrite Zabs_Zopp; auto with zarith.
Qed.
 
Theorem NotDividesDigit :
 forall r v : Z,
 (1 < r)%Z -> v <> 0%Z -> ~ Zdivides v (Zpower_nat r (digit r v)).
(* Goal: Zdivides n m *)
intros r v H H'; red in |- *; intros H'0; case H'0; intros q E.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
absurd (Zabs v < Zpower_nat r (digit r v))%Z; auto with zarith.
(* Goal: not (Z.lt (Z.abs v) (Zpower_nat r (digit r v))) *)
apply Zle_not_lt.
(* Goal: Z.le (Zpower_nat r (digit r v)) (Z.abs v) *)
case (Z_eq_dec q 0); intros Z1.
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r)))) (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.opp (Z.of_nat (Pos.to_nat n')))) (Z.opp (Z.of_nat (oZ r)))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
case H'; rewrite E; rewrite Z1; ring.
(* Goal: @eq Z (Z.mul p n) (Z.mul (Z.mul p m) q) *)
pattern v at 2 in |- *; rewrite E.
(* Goal: Z.le (Z.abs m) (Z.abs (Z.mul m q)) *)
rewrite Zabs_Zmult.
pattern (Zpower_nat r (digit r v)) at 1 in |- *;
 replace (Zpower_nat r (digit r v)) with (Zpower_nat r (digit r v) * 1)%Z;
 [ idtac | ring ].
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
rewrite (fun x y => Zabs_eq (Zpower_nat x y)); auto with zarith.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
apply Zle_Zmult_comp_l; auto with zarith.
generalize Z1; case q; simpl in |- *; try (intros H1; case H1; auto; fail);
 intros p;
 (case p; unfold Zle in |- *; simpl in |- *; intros; red in |- *; intros;
   discriminate).
Qed.
 
Theorem ZDividesLe :
 forall n m : Z, n <> 0%Z -> Zdivides n m -> (Zabs m <= Zabs n)%Z.
(* Goal: @eq Z (Z.mul p n) (Z.mul (Z.mul p m) q) *)
intros n m H' H'0; case H'0; intros q E; rewrite E.
(* Goal: Z.le (Z.abs m) (Z.abs (Z.mul m q)) *)
rewrite Zabs_Zmult.
pattern (Zabs m) at 1 in |- *; replace (Zabs m) with (Zabs m * 1)%Z;
 [ idtac | ring ].
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
apply Zle_Zmult_comp_l; auto with zarith.
generalize E H'; case q; simpl in |- *; auto;
 try (intros H1 H2; case H2; rewrite H1; ring; fail); 
 intros p; case p; unfold Zle in |- *; simpl in |- *; 
 intros; red in |- *; discriminate.
Qed.
 
Theorem Zquotient_mult_comp :
 forall m n p : Z, p <> 0%Z -> Zquotient (m * p) (n * p) = Zquotient m n.
(* Goal: forall (m n p : Z) (_ : not (@eq Z p Z0)), @eq Z (Zquotient (Z.mul m p) (Z.mul n p)) (Zquotient m n) *)
intros m n p Z1; case (Z_eq_dec n 0); intros Z2.
rewrite Z2; unfold Zquotient in |- *; case (m * p)%Z; case m; simpl in |- *;
 auto.
(* Goal: @eq Z (Zquotient (Z.mul m p) (Z.mul n p)) (Zquotient m n) *)
case (ZquotientProp m n); auto; intros r (H1, (H2, H3)).
apply sym_equal; apply ZquotientUnique with (r := (r * p)%Z);
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
 auto with zarith.
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r)))) (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.opp (Z.of_nat (Pos.to_nat n')))) (Z.opp (Z.of_nat (oZ r)))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
pattern m at 1 in |- *; rewrite H1; ring.
(* Goal: Z.le (Z.abs (Z.mul (Zquotient m n) (Z.mul n p))) (Z.abs (Z.mul m p)) *)
(* Goal: Z.lt (Z.abs (Z.mul r p)) (Z.abs (Z.mul n p)) *)
rewrite Zmult_assoc.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
repeat rewrite (fun x => Zabs_Zmult x p); auto with zarith.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
repeat rewrite Zabs_Zmult; auto with zarith.
(* Goal: @eq Z (Z.mul p (Z.mul m q)) (Z.mul (Z.mul p m) q) *)
apply Zmult_gt_0_lt_compat_r; auto with zarith.
apply Zlt_gt; generalize Z1; case p; simpl in |- *;
 try (intros H4; case H4; auto; fail); unfold Zlt in |- *; 
 simpl in |- *; auto; intros; red in |- *; intros; 
 discriminate.
Qed.
 
Theorem ZDivides_add :
 forall n m p : Z, Zdivides n p -> Zdivides m p -> Zdivides (n + m) p.
(* Goal: forall (n m p : Z) (_ : Zdivides n m) (_ : Zdivides m p), Zdivides n p *)
intros n m p H' H'0.
(* Goal: Zdivides n p *)
case H'; intros z1 Hz1.
(* Goal: Zdivides n p *)
case H'0; intros z2 Hz2.
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r)))) (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.opp (Z.of_nat (Pos.to_nat n')))) (Z.opp (Z.of_nat (oZ r)))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
exists (z1 + z2)%Z; rewrite Hz1; rewrite Hz2; ring.
Qed.
 
Theorem NDivides_minus :
 forall n m p : Z, Zdivides n p -> Zdivides m p -> Zdivides (n - m) p.
(* Goal: forall (n m p : Z) (_ : Zdivides n m) (_ : Zdivides m p), Zdivides n p *)
intros n m p H' H'0.
(* Goal: Zdivides n p *)
case H'; intros z1 Hz1.
(* Goal: Zdivides n p *)
case H'0; intros z2 Hz2.
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r)))) (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.opp (Z.of_nat (Pos.to_nat n')))) (Z.opp (Z.of_nat (oZ r)))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
exists (z1 - z2)%Z; rewrite Hz1; rewrite Hz2; ring.
Qed.
 
Theorem ZDivides_mult :
 forall n m p q : Z, Zdivides n p -> Zdivides m q -> Zdivides (n * m) (p * q).
(* Goal: forall (n m p q : Z) (_ : Zdivides n p) (_ : Zdivides m q), Zdivides (Z.mul n m) (Z.mul p q) *)
intros n m p q H' H'0.
(* Goal: Zdivides n p *)
case H'; intros z1 Hz1.
(* Goal: Zdivides n p *)
case H'0; intros z2 Hz2.
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r)))) (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.opp (Z.of_nat (Pos.to_nat n')))) (Z.opp (Z.of_nat (oZ r)))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
exists (z1 * z2)%Z; rewrite Hz1; rewrite Hz2; ring.
Qed.
 
Theorem ZdividesTrans :
 forall n m p : Z, Zdivides n m -> Zdivides m p -> Zdivides n p.
(* Goal: forall (n m p : Z) (_ : Zdivides n m) (_ : Zdivides m p), Zdivides n p *)
intros n m p H' H'0.
(* Goal: Zdivides n p *)
case H'; intros z1 Hz1.
(* Goal: Zdivides n p *)
case H'0; intros z2 Hz2.
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.of_nat (Pos.to_nat n'))) (Z.of_nat (oZ r)))) (Z.add (Z.mul (Z.of_nat (oZ q)) (Z.opp (Z.of_nat (Pos.to_nat n')))) (Z.opp (Z.of_nat (oZ r)))) *)
(* Goal: Z.le (Z.abs (Z.mul (oZ1 q) (Zneg n'))) (Zpos m') *)
(* Goal: Z.lt (Z.abs (Z.opp (oZ1 r))) (Zpos n') *)
exists (z1 * z2)%Z; rewrite Hz1; rewrite Hz2; ring.
Qed.
 
Theorem ZdividesLessPow :
 forall (n : Z) (m p : nat),
 m <= p -> Zdivides (Zpower_nat n p) (Zpower_nat n m).
(* Goal: forall (n : Z) (m p : nat) (_ : le m p), Zdivides (Zpower_nat n p) (Zpower_nat n m) *)
intros n m p H'; exists (Zpower_nat n (p - m)).
(* Goal: @eq Z (Zpower_nat n p) (Z.mul (Zpower_nat n m) (Zpower_nat n (Init.Nat.sub p m))) *)
rewrite <- Zpower_nat_is_exp.
(* Goal: @eq Z (Zpower_nat n p) (Zpower_nat n (Init.Nat.add m (Init.Nat.sub p m))) *)
rewrite <- le_plus_minus; auto.
Qed.
