(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(**
   natZ.
   Some lemmas about inject_nat, absolu and the relation between
   Z and nat in general.
 
   @author Olga Caprotti and Martijn Oostdijk
   @version $Revision$
*)

Require Import ZArith.
Require Import EqNat.

Require Import lemmas.

Lemma abs_opp : forall x : Z, Zabs_nat x = Zabs_nat (- x).
Proof.
(* Goal: forall (x : Z) (_ : not (@eq Z x Z0)), lt O (Z.abs_nat x) *)
   simple induction x.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *. reflexivity.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *. reflexivity.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *. reflexivity.
Qed.

Lemma inj_abs_pos : forall x : Z, (x >= 0)%Z -> Z_of_nat (Zabs_nat x) = x.
Proof.
(* Goal: forall (x : Z) (_ : not (@eq Z x Z0)), lt O (Z.abs_nat x) *)
   simple induction x.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   intros. simpl in |- *.
   induction  p as [p Hrecp| p Hrecp| ].
(* Goal: @eq Z (Z.of_nat (Pos.to_nat (xI p))) (Zpos (xI p)) *)
(* Goal: @eq Z (Z.of_nat (Pos.to_nat (xO p))) (Zpos (xO p)) *)
(* Goal: @eq Z (Z.of_nat (Pos.to_nat xH)) (Zpos xH) *)
(* Goal: forall (p : positive) (_ : Z.ge (Zneg p) Z0), @eq Z (Z.of_nat (Z.abs_nat (Zneg p))) (Zneg p) *)
   rewrite BinInt.Zpos_xI.
(* Goal: @eq Z (Z.of_nat (Pos.to_nat (xO p))) (Z.mul (Zpos (xO xH)) (Zpos p)) *)
(* Goal: @eq Z (Z.of_nat (Pos.to_nat xH)) (Zpos xH) *)
(* Goal: forall (p : positive) (_ : Z.ge (Zneg p) Z0), @eq Z (Z.of_nat (Z.abs_nat (Zneg p))) (Zneg p) *)
   rewrite <- Hrecp.
(* Goal: @eq Z (Z.of_nat (Pos.to_nat (xI p))) (Z.add (Z.mul (Zpos (xO xH)) (Z.of_nat (Pos.to_nat p))) (Zpos xH)) *)
(* Goal: Z.ge (Zpos p) Z0 *)
(* Goal: @eq Z (Z.of_nat (Pos.to_nat (xO p))) (Zpos (xO p)) *)
(* Goal: @eq Z (Z.of_nat (Pos.to_nat xH)) (Zpos xH) *)
(* Goal: forall (p : positive) (_ : Z.ge (Zneg p) Z0), @eq Z (Z.of_nat (Z.abs_nat (Zneg p))) (Zneg p) *)
   replace (nat_of_P (xI p)) with (S (2 * nat_of_P p)).
(* Goal: @eq Z (Z.of_nat (S (Init.Nat.mul (S (S O)) (Pos.to_nat p)))) (Z.add (Z.mul (Zpos (xO xH)) (Z.of_nat (Pos.to_nat p))) (Zpos xH)) *)
(* Goal: @eq nat (S (Init.Nat.mul (S (S O)) (Pos.to_nat p))) (Pos.to_nat (xI p)) *)
(* Goal: Z.ge (Zpos p) Z0 *)
(* Goal: @eq Z (Z.of_nat (Pos.to_nat (xO p))) (Zpos (xO p)) *)
(* Goal: @eq Z (Z.of_nat (Pos.to_nat xH)) (Zpos xH) *)
(* Goal: forall (p : positive) (_ : Z.ge (Zneg p) Z0), @eq Z (Z.of_nat (Z.abs_nat (Zneg p))) (Zneg p) *)
   rewrite Znat.inj_S.
(* Goal: @eq Z (Z.of_nat (Init.Nat.mul (S (S O)) (Pos.to_nat p))) (Z.mul (Zpos (xO xH)) (Z.of_nat (Pos.to_nat p))) *)
(* Goal: @eq nat (Init.Nat.mul (S (S O)) (Pos.to_nat p)) (Pos.to_nat (xO p)) *)
(* Goal: Z.ge (Zpos p) Z0 *)
(* Goal: @eq Z (Z.of_nat (Pos.to_nat xH)) (Zpos xH) *)
(* Goal: forall (p : positive) (_ : Z.ge (Zneg p) Z0), @eq Z (Z.of_nat (Z.abs_nat (Zneg p))) (Zneg p) *)
   rewrite Znat.inj_mult.
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Z.of_nat (Pos.to_nat p))) (Z.mul (Zpos (xO xH)) (Z.of_nat (Pos.to_nat p))) *)
(* Goal: @eq nat (Init.Nat.mul (S (S O)) (Pos.to_nat p)) (Pos.to_nat (xO p)) *)
(* Goal: Z.ge (Zpos p) Z0 *)
(* Goal: @eq Z (Z.of_nat (Pos.to_nat xH)) (Zpos xH) *)
(* Goal: forall (p : positive) (_ : Z.ge (Zneg p) Z0), @eq Z (Z.of_nat (Z.abs_nat (Zneg p))) (Zneg p) *)
   rewrite Hrecp.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
(* Goal: Z.ge x (Zpos xH) *)
   apply Zle_ge. apply Zorder.Zle_0_pos.
(* Goal: @eq nat (Init.Nat.mul (S (S O)) (Pos.to_nat p)) (Pos.to_nat (xO p)) *)
(* Goal: Z.ge (Zpos p) Z0 *)
(* Goal: @eq Z (Z.of_nat (Pos.to_nat xH)) (Zpos xH) *)
(* Goal: forall (p : positive) (_ : Z.ge (Zneg p) Z0), @eq Z (Z.of_nat (Z.abs_nat (Zneg p))) (Zneg p) *)
   replace 2 with (nat_of_P 2).
(* Goal: @eq nat (Pos.to_nat (Pos.mul p p0)) (Init.Nat.mul (Pos.to_nat p) (Pos.to_nat p0)) *)
   rewrite <- nat_of_P_mult_morphism.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *.
(* Goal: @eq nat (S (Pos.to_nat (xO p))) (Pos.to_nat (xI p)) *)
(* Goal: @eq nat (Pos.to_nat (xO xH)) (S (S O)) *)
(* Goal: Z.ge (Zpos p) Z0 *)
(* Goal: @eq Z (Z.of_nat (Pos.to_nat (xO p))) (Zpos (xO p)) *)
(* Goal: @eq Z (Z.of_nat (Pos.to_nat xH)) (Zpos xH) *)
(* Goal: forall (p : positive) (_ : Z.ge (Zneg p) Z0), @eq Z (Z.of_nat (Z.abs_nat (Zneg p))) (Zneg p) *)
   rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ.
(* Goal: @eq nat (Pos.to_nat (Pos.of_succ_nat (Pos.to_nat (xO p)))) (Pos.to_nat (xI p)) *)
(* Goal: @eq nat (Pos.to_nat (xO xH)) (S (S O)) *)
(* Goal: Z.ge (Zpos p) Z0 *)
(* Goal: @eq Z (Z.of_nat (Pos.to_nat (xO p))) (Zpos (xO p)) *)
(* Goal: @eq Z (Z.of_nat (Pos.to_nat xH)) (Zpos xH) *)
(* Goal: forall (p : positive) (_ : Z.ge (Zneg p) Z0), @eq Z (Z.of_nat (Z.abs_nat (Zneg p))) (Zneg p) *)
   rewrite P_of_succ_nat_o_nat_of_P_eq_succ.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
(* Goal: Z.ge x (Zpos xH) *)
   apply Zle_ge. apply Zorder.Zle_0_pos.
(* Goal: @eq Z (Z.of_nat (Pos.to_nat (xO p))) (Zpos (xO p)) *)
(* Goal: @eq Z (Z.of_nat (Pos.to_nat xH)) (Zpos xH) *)
(* Goal: forall (p : positive) (_ : Z.ge (Zneg p) Z0), @eq Z (Z.of_nat (Z.abs_nat (Zneg p))) (Zneg p) *)
   rewrite BinInt.Zpos_xO.
(* Goal: @eq Z (Z.of_nat (Pos.to_nat (xO p))) (Z.mul (Zpos (xO xH)) (Zpos p)) *)
(* Goal: @eq Z (Z.of_nat (Pos.to_nat xH)) (Zpos xH) *)
(* Goal: forall (p : positive) (_ : Z.ge (Zneg p) Z0), @eq Z (Z.of_nat (Z.abs_nat (Zneg p))) (Zneg p) *)
   rewrite <- Hrecp.
(* Goal: @eq Z (Z.of_nat (Pos.to_nat (xO p))) (Z.mul (Zpos (xO xH)) (Z.of_nat (Pos.to_nat p))) *)
(* Goal: Z.ge (Zpos p) Z0 *)
(* Goal: @eq Z (Z.of_nat (Pos.to_nat xH)) (Zpos xH) *)
(* Goal: forall (p : positive) (_ : Z.ge (Zneg p) Z0), @eq Z (Z.of_nat (Z.abs_nat (Zneg p))) (Zneg p) *)
   replace (nat_of_P (xO p)) with (2 * nat_of_P p).
(* Goal: @eq Z (Z.of_nat (Init.Nat.mul (S (S O)) (Pos.to_nat p))) (Z.mul (Zpos (xO xH)) (Z.of_nat (Pos.to_nat p))) *)
(* Goal: @eq nat (Init.Nat.mul (S (S O)) (Pos.to_nat p)) (Pos.to_nat (xO p)) *)
(* Goal: Z.ge (Zpos p) Z0 *)
(* Goal: @eq Z (Z.of_nat (Pos.to_nat xH)) (Zpos xH) *)
(* Goal: forall (p : positive) (_ : Z.ge (Zneg p) Z0), @eq Z (Z.of_nat (Z.abs_nat (Zneg p))) (Zneg p) *)
   rewrite Znat.inj_mult.
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Z.of_nat (Pos.to_nat p))) (Z.mul (Zpos (xO xH)) (Z.of_nat (Pos.to_nat p))) *)
(* Goal: @eq nat (Init.Nat.mul (S (S O)) (Pos.to_nat p)) (Pos.to_nat (xO p)) *)
(* Goal: Z.ge (Zpos p) Z0 *)
(* Goal: @eq Z (Z.of_nat (Pos.to_nat xH)) (Zpos xH) *)
(* Goal: forall (p : positive) (_ : Z.ge (Zneg p) Z0), @eq Z (Z.of_nat (Z.abs_nat (Zneg p))) (Zneg p) *)
   rewrite Hrecp.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
(* Goal: Z.ge x (Zpos xH) *)
   apply Zle_ge. apply Zorder.Zle_0_pos.
(* Goal: @eq nat (Init.Nat.mul (S (S O)) (Pos.to_nat p)) (Pos.to_nat (xO p)) *)
(* Goal: Z.ge (Zpos p) Z0 *)
(* Goal: @eq Z (Z.of_nat (Pos.to_nat xH)) (Zpos xH) *)
(* Goal: forall (p : positive) (_ : Z.ge (Zneg p) Z0), @eq Z (Z.of_nat (Z.abs_nat (Zneg p))) (Zneg p) *)
   replace 2 with (nat_of_P 2).
(* Goal: @eq nat (Pos.to_nat (Pos.mul p p0)) (Init.Nat.mul (Pos.to_nat p) (Pos.to_nat p0)) *)
   rewrite <- nat_of_P_mult_morphism.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
(* Goal: Z.ge x (Zpos xH) *)
   apply Zle_ge.
(* Goal: Z.le Z0 (Zpos p) *)
(* Goal: @eq Z (Z.of_nat (Pos.to_nat xH)) (Zpos xH) *)
(* Goal: forall (p : positive) (_ : Z.ge (Zneg p) Z0), @eq Z (Z.of_nat (Z.abs_nat (Zneg p))) (Zneg p) *)
   apply Zorder.Zle_0_pos.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intros.
(* Goal: lt O (Z.abs_nat Z0) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zpos p) Z0)), lt O (Z.abs_nat (Zpos p)) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   elim H.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
Qed.

Lemma inj_abs_neg :
 forall x : Z, (x < 0)%Z -> Z_of_nat (Zabs_nat x) = (- x)%Z.
Proof.
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intros.
(* Goal: @eq Z (Z.of_nat (Z.abs_nat x)) (Z.opp x) *)
   rewrite abs_opp.
(* Goal: @eq Z (Z.of_nat (Z.abs_nat (Z.opp x))) (Z.opp x) *)
   apply inj_abs_pos.
(* Goal: Z.ge x (Zpos xH) *)
   apply Zle_ge.
(* Goal: Z.le Z0 (Z.opp x) *)
   apply Zplus_le_reg_l with x.
(* Goal: Z.le (Z.add x Z0) (Z.add x (Z.opp x)) *)
   rewrite <- Zplus_0_r_reverse.
(* Goal: Z.le x (Z.add x (Z.opp x)) *)
   rewrite Zplus_opp_r.
(* Goal: Z.le Z0 x *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.ge x (Zpos xH) *)
   apply Zlt_le_weak.
(* Goal: Z.lt Z0 x *)
   assumption.
Qed.

Lemma abs_inj : forall n : nat, Zabs_nat (Z_of_nat n) = n.
Proof.
(* Goal: forall n : nat, Z.ge (Z.of_nat n) Z0 *)
   simple induction n.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *. reflexivity.
(* Goal: forall (n : nat) (_ : @eq nat (Z.abs_nat (Z.of_nat n)) n), @eq nat (Z.abs_nat (Z.of_nat (S n))) (S n) *)
   intros m IH.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   rewrite <- IH. simpl in |- *.
(* Goal: @eq nat (Pos.to_nat (Pos.of_succ_nat (Z.abs_nat (Z.of_nat m)))) (S (Z.abs_nat (Z.of_nat m))) *)
   rewrite nat_of_P_o_P_of_succ_nat_eq_succ.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
Qed.

Lemma abs_mult : forall x y : Z, Zabs_nat (x * y) = Zabs_nat x * Zabs_nat y.
Proof.
(* Goal: forall (x : Z) (_ : not (@eq Z x Z0)), lt O (Z.abs_nat x) *)
   simple induction x.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *. intro. reflexivity.
(* Goal: forall _ : not (@eq Z Z0 Z0), lt O (Z.abs_nat Z0) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zpos p) Z0)), lt O (Z.abs_nat (Zpos p)) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intro.
(* Goal: forall (y : Z) (_ : Z.le Z0 (Zpos p)) (_ : Z.le Z0 y), @eq nat (Z.abs_nat (Z.add (Zpos p) y)) (Init.Nat.add (Z.abs_nat (Zpos p)) (Z.abs_nat y)) *)
(* Goal: forall (p : positive) (y : Z) (_ : Z.le Z0 (Zneg p)) (_ : Z.le Z0 y), @eq nat (Z.abs_nat (Z.add (Zneg p) y)) (Init.Nat.add (Z.abs_nat (Zneg p)) (Z.abs_nat y)) *)
   simple induction y.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *.
(* Goal: @eq nat O (Init.Nat.mul (Pos.to_nat p) O) *)
(* Goal: forall p0 : positive, @eq nat (Z.abs_nat (Z.mul (Zneg p) (Zpos p0))) (Init.Nat.mul (Z.abs_nat (Zneg p)) (Z.abs_nat (Zpos p0))) *)
(* Goal: forall p0 : positive, @eq nat (Z.abs_nat (Z.mul (Zneg p) (Zneg p0))) (Init.Nat.mul (Z.abs_nat (Zneg p)) (Z.abs_nat (Zneg p0))) *)
   rewrite <- mult_n_O.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
(* Goal: forall _ : not (@eq Z Z0 Z0), lt O (Z.abs_nat Z0) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zpos p) Z0)), lt O (Z.abs_nat (Zpos p)) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intro.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *.
(* Goal: @eq nat (Pos.to_nat (Pos.mul p p0)) (Init.Nat.mul (Pos.to_nat p) (Pos.to_nat p0)) *)
   rewrite <- nat_of_P_mult_morphism.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *.
(* Goal: forall _ : not (@eq Z Z0 Z0), lt O (Z.abs_nat Z0) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zpos p) Z0)), lt O (Z.abs_nat (Zpos p)) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intro.
(* Goal: @eq nat (Pos.to_nat (Pos.mul p p0)) (Init.Nat.mul (Pos.to_nat p) (Pos.to_nat p0)) *)
   rewrite <- nat_of_P_mult_morphism.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
(* Goal: forall _ : not (@eq Z Z0 Z0), lt O (Z.abs_nat Z0) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zpos p) Z0)), lt O (Z.abs_nat (Zpos p)) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intro.
(* Goal: forall (y : Z) (_ : Z.le Z0 (Zpos p)) (_ : Z.le Z0 y), @eq nat (Z.abs_nat (Z.add (Zpos p) y)) (Init.Nat.add (Z.abs_nat (Zpos p)) (Z.abs_nat y)) *)
(* Goal: forall (p : positive) (y : Z) (_ : Z.le Z0 (Zneg p)) (_ : Z.le Z0 y), @eq nat (Z.abs_nat (Z.add (Zneg p) y)) (Init.Nat.add (Z.abs_nat (Zneg p)) (Z.abs_nat y)) *)
   simple induction y.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *.
(* Goal: @eq nat O (Init.Nat.mul (Pos.to_nat p) O) *)
(* Goal: forall p0 : positive, @eq nat (Z.abs_nat (Z.mul (Zneg p) (Zpos p0))) (Init.Nat.mul (Z.abs_nat (Zneg p)) (Z.abs_nat (Zpos p0))) *)
(* Goal: forall p0 : positive, @eq nat (Z.abs_nat (Z.mul (Zneg p) (Zneg p0))) (Init.Nat.mul (Z.abs_nat (Zneg p)) (Z.abs_nat (Zneg p0))) *)
   rewrite <- mult_n_O.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
(* Goal: forall _ : not (@eq Z Z0 Z0), lt O (Z.abs_nat Z0) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zpos p) Z0)), lt O (Z.abs_nat (Zpos p)) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intro.
(* Goal: @eq nat (Z.abs_nat (Z.mul (Zneg p) (Zneg p0))) (Init.Nat.mul (Z.abs_nat (Zneg p)) (Z.abs_nat (Zneg p0))) *)
   unfold Zabs_nat in |- *.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *.
(* Goal: @eq nat (Pos.to_nat (Pos.mul p p0)) (Init.Nat.mul (Pos.to_nat p) (Pos.to_nat p0)) *)
   rewrite <- nat_of_P_mult_morphism.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
(* Goal: forall _ : not (@eq Z Z0 Z0), lt O (Z.abs_nat Z0) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zpos p) Z0)), lt O (Z.abs_nat (Zpos p)) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intro.
(* Goal: @eq nat (Z.abs_nat (Z.mul (Zneg p) (Zneg p0))) (Init.Nat.mul (Z.abs_nat (Zneg p)) (Z.abs_nat (Zneg p0))) *)
   unfold Zabs_nat in |- *.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *.
(* Goal: @eq nat (Pos.to_nat (Pos.mul p p0)) (Init.Nat.mul (Pos.to_nat p) (Pos.to_nat p0)) *)
   rewrite <- nat_of_P_mult_morphism.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
Qed.

Lemma isnat_inj_abs :
 forall (x : Z) (n : nat), x = Z_of_nat n -> n = Zabs_nat x.
Proof.
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intros.
(* Goal: @eq nat n (Z.abs_nat x) *)
   rewrite H.
(* Goal: @eq nat (Init.Nat.sub nx ny) (Init.Nat.sub nx (Z.abs_nat (Z.of_nat ny))) *)
(* Goal: le ny nx *)
(* Goal: Z.le Z0 (Z.sub x y) *)
(* Goal: Z.le Z0 y *)
(* Goal: Z.le Z0 x *)
   rewrite abs_inj.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
Qed.

Lemma isnat_abs_inj :
 forall (x : Z) (n : nat), (0 <= x)%Z -> n = Zabs_nat x -> x = Z_of_nat n.
Proof.
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intros.
(* Goal: @eq Z x (Z.of_nat n) *)
   rewrite H0.
(* Goal: @eq Z x (Z.of_nat (Z.abs_nat x)) *)
   rewrite inj_abs_pos.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
(* Goal: Z.ge x (Zpos xH) *)
   apply Zle_ge.
(* Goal: Z.lt Z0 x *)
   assumption.
Qed.

Lemma isnat_plus : forall x y : Z, (0 <= x)%Z -> (0 <= y)%Z -> (0 <= x + y)%Z.
Proof.
(* Goal: forall (x : Z) (_ : not (@eq Z x Z0)), lt O (Z.abs_nat x) *)
   simple induction x. simpl in |- *. intros. assumption.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   intro. simple induction y. simpl in |- *. intros. assumption.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *. intros. unfold Zle in |- *. simpl in |- *. discriminate.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   intros. unfold Zle in H0. elim H0. simpl in |- *. reflexivity.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   intros. unfold Zle in H. elim H. simpl in |- *. reflexivity.
Qed.

Lemma isnat_mult : forall x y : Z, (0 <= x)%Z -> (0 <= y)%Z -> (0 <= x * y)%Z.
Proof.
(* Goal: forall (x : Z) (_ : not (@eq Z x Z0)), lt O (Z.abs_nat x) *)
   simple induction x.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *. intros. unfold Zle in |- *. simpl in |- *. discriminate.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   intro. simple induction y. simpl in |- *. intros. unfold Zle in |- *. simpl in |- *. discriminate.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *. intros. unfold Zle in |- *. simpl in |- *. discriminate.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   intros. unfold Zle in H0. elim H0. simpl in |- *. reflexivity.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   intros. unfold Zle in H. elim H. simpl in |- *. reflexivity.
Qed.


Lemma lezle :
 forall x y : Z,
 (0 <= x)%Z -> (0 <= y)%Z -> (x <= y)%Z -> Zabs_nat x <= Zabs_nat y.
Proof.
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intros.
(* Goal: gt (Z.abs_nat x) (Z.abs_nat y) *)
   elim (le_or_lt (Zabs_nat x) (Zabs_nat y)).
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intros. assumption.
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intros. elim (Zlt_not_le y x).
(* Goal: Z.le x y *)
(* Goal: Z.lt y x *)
(* Goal: forall _ : lt (Z.abs_nat y) (Z.abs_nat x), gt (Z.abs_nat x) (Z.abs_nat y) *)
   rewrite <- (inj_abs_pos x).
(* Goal: Z.le (Z.of_nat (Z.abs_nat x)) y *)
(* Goal: Z.ge x Z0 *)
(* Goal: Z.lt y x *)
(* Goal: forall _ : lt (Z.abs_nat y) (Z.abs_nat x), gt (Z.abs_nat x) (Z.abs_nat y) *)
   rewrite <- (inj_abs_pos y).
(* Goal: Z.lt Z0 x *)
   apply Znat.inj_lt. assumption.
(* Goal: Z.ge x (Zpos xH) *)
   apply Zle_ge. assumption.
(* Goal: Z.ge x (Zpos xH) *)
   apply Zle_ge. assumption.
(* Goal: Z.lt Z0 x *)
   assumption.
Qed.

Lemma gtzgt :
 forall x y : Z,
 (0 <= x)%Z -> (0 <= y)%Z -> (x > y)%Z -> Zabs_nat x > Zabs_nat y.
Proof.
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intros.
(* Goal: gt (Z.abs_nat x) (Z.abs_nat y) *)
   elim (le_or_lt (Zabs_nat x) (Zabs_nat y)).
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intros.
(* Goal: gt (Z.abs_nat x) (Z.abs_nat y) *)
(* Goal: forall _ : lt (Z.abs_nat y) (Z.abs_nat x), gt (Z.abs_nat x) (Z.abs_nat y) *)
   elim (Zle_not_lt x y).
(* Goal: Z.le x y *)
(* Goal: Z.lt y x *)
(* Goal: forall _ : lt (Z.abs_nat y) (Z.abs_nat x), gt (Z.abs_nat x) (Z.abs_nat y) *)
   rewrite <- (inj_abs_pos x).
(* Goal: Z.le (Z.of_nat (Z.abs_nat x)) y *)
(* Goal: Z.ge x Z0 *)
(* Goal: Z.lt y x *)
(* Goal: forall _ : lt (Z.abs_nat y) (Z.abs_nat x), gt (Z.abs_nat x) (Z.abs_nat y) *)
   rewrite <- (inj_abs_pos y).
(* Goal: Z.lt Z0 x *)
   apply Znat.inj_le. assumption.
(* Goal: Z.ge x (Zpos xH) *)
   apply Zle_ge. assumption.
(* Goal: Z.ge x (Zpos xH) *)
   apply Zle_ge. assumption.
(* Goal: Z.lt Z0 x *)
   apply Zgt_lt. assumption.
(* Goal: Z.lt Z0 x *)
   unfold gt in |- *. intro. assumption.
Qed.

Lemma ltzlt :
 forall x y : Z,
 (0 <= x)%Z -> (0 <= y)%Z -> (x < y)%Z -> Zabs_nat x < Zabs_nat y.
Proof.
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intros.
(* Goal: lt (Z.abs_nat x) (Z.abs_nat y) *)
   change (Zabs_nat y > Zabs_nat x) in |- *.
(* Goal: Z.lt Z0 x *)
   apply gtzgt. assumption. assumption.
(* Goal: Z.lt Z0 x *)
   apply Zlt_gt. assumption.
Qed.

Lemma abs_plus_pos :
 forall x y : Z,
 (0 <= x)%Z -> (0 <= y)%Z -> Zabs_nat (x + y) = Zabs_nat x + Zabs_nat y.
Proof.
(* Goal: forall (x : Z) (_ : not (@eq Z x Z0)), lt O (Z.abs_nat x) *)
   simple induction x.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *.
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intros.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
(* Goal: forall _ : not (@eq Z Z0 Z0), lt O (Z.abs_nat Z0) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zpos p) Z0)), lt O (Z.abs_nat (Zpos p)) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intro.
(* Goal: forall (y : Z) (_ : Z.le Z0 (Zpos p)) (_ : Z.le Z0 y), @eq nat (Z.abs_nat (Z.add (Zpos p) y)) (Init.Nat.add (Z.abs_nat (Zpos p)) (Z.abs_nat y)) *)
(* Goal: forall (p : positive) (y : Z) (_ : Z.le Z0 (Zneg p)) (_ : Z.le Z0 y), @eq nat (Z.abs_nat (Z.add (Zneg p) y)) (Init.Nat.add (Z.abs_nat (Zneg p)) (Z.abs_nat y)) *)
   simple induction y.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *.
(* Goal: forall (_ : Z.le Z0 (Zpos p)) (_ : Z.le Z0 Z0), @eq nat (Pos.to_nat p) (Init.Nat.add (Pos.to_nat p) O) *)
(* Goal: forall (p0 : positive) (_ : Z.le Z0 (Zpos p)) (_ : Z.le Z0 (Zpos p0)), @eq nat (Z.abs_nat (Z.add (Zpos p) (Zpos p0))) (Init.Nat.add (Z.abs_nat (Zpos p)) (Z.abs_nat (Zpos p0))) *)
(* Goal: forall (p0 : positive) (_ : Z.le Z0 (Zpos p)) (_ : Z.le Z0 (Zneg p0)), @eq nat (Z.abs_nat (Z.add (Zpos p) (Zneg p0))) (Init.Nat.add (Z.abs_nat (Zpos p)) (Z.abs_nat (Zneg p0))) *)
(* Goal: forall (p : positive) (y : Z) (_ : Z.le Z0 (Zneg p)) (_ : Z.le Z0 y), @eq nat (Z.abs_nat (Z.add (Zneg p) y)) (Init.Nat.add (Z.abs_nat (Zneg p)) (Z.abs_nat y)) *)
   rewrite <- plus_n_O.
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intros.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *.
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intros.
(* Goal: @eq nat (Pos.to_nat (Pos.add p p0)) (Init.Nat.add (Pos.to_nat p) (Pos.to_nat p0)) *)
(* Goal: forall (p0 : positive) (_ : Z.le Z0 (Zpos p)) (_ : Z.le Z0 (Zneg p0)), @eq nat (Z.abs_nat (Z.add (Zpos p) (Zneg p0))) (Init.Nat.add (Z.abs_nat (Zpos p)) (Z.abs_nat (Zneg p0))) *)
(* Goal: forall (p : positive) (y : Z) (_ : Z.le Z0 (Zneg p)) (_ : Z.le Z0 y), @eq nat (Z.abs_nat (Z.add (Zneg p) y)) (Init.Nat.add (Z.abs_nat (Zneg p)) (Z.abs_nat y)) *)
   apply nat_of_P_plus_morphism.
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intros.
(* Goal: @eq nat (Z.abs_nat (Z.add (Zpos p) (Zneg p0))) (Init.Nat.add (Z.abs_nat (Zpos p)) (Z.abs_nat (Zneg p0))) *)
(* Goal: forall (p : positive) (y : Z) (_ : Z.le Z0 (Zneg p)) (_ : Z.le Z0 y), @eq nat (Z.abs_nat (Z.add (Zneg p) y)) (Init.Nat.add (Z.abs_nat (Zneg p)) (Z.abs_nat y)) *)
   unfold Zle in H0.
(* Goal: @eq nat (Z.abs_nat (Z.add (Zpos p) (Zneg p0))) (Init.Nat.add (Z.abs_nat (Zpos p)) (Z.abs_nat (Zneg p0))) *)
(* Goal: forall (p : positive) (y : Z) (_ : Z.le Z0 (Zneg p)) (_ : Z.le Z0 y), @eq nat (Z.abs_nat (Z.add (Zneg p) y)) (Init.Nat.add (Z.abs_nat (Zneg p)) (Z.abs_nat y)) *)
   simpl in H0.
(* Goal: @eq nat (Z.abs_nat (Z.add (Zpos p) (Zneg p0))) (Init.Nat.add (Z.abs_nat (Zpos p)) (Z.abs_nat (Zneg p0))) *)
(* Goal: forall (p : positive) (y : Z) (_ : Z.le Z0 (Zneg p)) (_ : Z.le Z0 y), @eq nat (Z.abs_nat (Z.add (Zneg p) y)) (Init.Nat.add (Z.abs_nat (Zneg p)) (Z.abs_nat y)) *)
   elim H0.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intros.
(* Goal: @eq nat (Z.abs_nat (Z.add (Zneg p) y)) (Init.Nat.add (Z.abs_nat (Zneg p)) (Z.abs_nat y)) *)
   unfold Zle in H.
(* Goal: @eq nat (Z.abs_nat (Z.add (Zneg p) y)) (Init.Nat.add (Z.abs_nat (Zneg p)) (Z.abs_nat y)) *)
   simpl in H.
(* Goal: lt O (Z.abs_nat Z0) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zpos p) Z0)), lt O (Z.abs_nat (Zpos p)) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   elim H.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
Qed.

Lemma abs_minus_pos :
 forall x y : Z,
 (0 <= x)%Z ->
 (0 <= y)%Z -> (x >= y)%Z -> Zabs_nat (x - y) = Zabs_nat x - Zabs_nat y.
Proof.
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intros.
(* Goal: @eq nat (Z.abs_nat (Z.sub x y)) (Init.Nat.sub (Z.abs_nat x) (Z.abs_nat y)) *)
   elim (Z_of_nat_complete x).
(* Goal: forall (x0 : nat) (_ : @eq Z x (Z.of_nat x0)), @eq nat (Z.abs_nat (Z.sub x y)) (Init.Nat.sub (Z.abs_nat x) (Z.abs_nat y)) *)
(* Goal: Z.le Z0 x *)
   intros nx Hx.
(* Goal: @eq nat (Z.abs_nat (Z.sub x y)) (Init.Nat.sub (Z.abs_nat x) (Z.abs_nat y)) *)
(* Goal: Z.le Z0 x *)
   elim (Z_of_nat_complete y).
(* Goal: forall (x0 : nat) (_ : @eq Z y (Z.of_nat x0)), @eq nat (Z.abs_nat (Z.sub x y)) (Init.Nat.sub (Z.abs_nat x) (Z.abs_nat y)) *)
(* Goal: Z.le Z0 y *)
(* Goal: Z.le Z0 x *)
   intros ny Hy.
(* Goal: @eq nat (Z.abs_nat (Z.sub x y)) (Init.Nat.sub (Z.abs_nat x) (Z.abs_nat y)) *)
(* Goal: Z.le Z0 y *)
(* Goal: Z.le Z0 x *)
   elim (Z_of_nat_complete (x - y)).
(* Goal: forall (x0 : nat) (_ : @eq Z (Z.sub x y) (Z.of_nat x0)), @eq nat (Z.abs_nat (Z.sub x y)) (Init.Nat.sub (Z.abs_nat x) (Z.abs_nat y)) *)
(* Goal: Z.le Z0 (Z.sub x y) *)
(* Goal: Z.le Z0 y *)
(* Goal: Z.le Z0 x *)
   intros d Hd.
(* Goal: @eq nat (Z.abs_nat (Z.sub x y)) (Init.Nat.sub (Z.abs_nat x) (Z.abs_nat y)) *)
(* Goal: Z.le Z0 (Z.sub x y) *)
(* Goal: Z.le Z0 y *)
(* Goal: Z.le Z0 x *)
   rewrite Hx.
(* Goal: @eq nat (Z.abs_nat (Z.sub (Z.of_nat nx) y)) (Init.Nat.sub (Z.abs_nat (Z.of_nat nx)) (Z.abs_nat y)) *)
(* Goal: Z.le Z0 (Z.sub x y) *)
(* Goal: Z.le Z0 y *)
(* Goal: Z.le Z0 x *)
   rewrite Hy.
(* Goal: @eq nat (Z.abs_nat (Z.sub (Z.of_nat nx) (Z.of_nat ny))) (Init.Nat.sub (Z.abs_nat (Z.of_nat nx)) (Z.abs_nat (Z.of_nat ny))) *)
(* Goal: Z.le Z0 (Z.sub x y) *)
(* Goal: Z.le Z0 y *)
(* Goal: Z.le Z0 x *)
   rewrite <- Znat.inj_minus1.
(* Goal: @eq nat (Init.Nat.sub nx ny) (Init.Nat.sub nx (Z.abs_nat (Z.of_nat ny))) *)
(* Goal: le ny nx *)
(* Goal: Z.le Z0 (Z.sub x y) *)
(* Goal: Z.le Z0 y *)
(* Goal: Z.le Z0 x *)
   rewrite abs_inj.
(* Goal: @eq nat (Init.Nat.sub nx ny) (Init.Nat.sub nx (Z.abs_nat (Z.of_nat ny))) *)
(* Goal: le ny nx *)
(* Goal: Z.le Z0 (Z.sub x y) *)
(* Goal: Z.le Z0 y *)
(* Goal: Z.le Z0 x *)
   rewrite abs_inj.
(* Goal: @eq nat (Init.Nat.sub nx ny) (Init.Nat.sub nx (Z.abs_nat (Z.of_nat ny))) *)
(* Goal: le ny nx *)
(* Goal: Z.le Z0 (Z.sub x y) *)
(* Goal: Z.le Z0 y *)
(* Goal: Z.le Z0 x *)
   rewrite abs_inj.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
(* Goal: le ny nx *)
(* Goal: Z.le Z0 (Z.sub x y) *)
(* Goal: Z.le Z0 y *)
(* Goal: Z.le Z0 x *)
   rewrite (isnat_inj_abs x nx).
(* Goal: le ny (Z.abs_nat x) *)
(* Goal: @eq Z x (Z.of_nat nx) *)
(* Goal: Z.le Z0 (Z.sub x y) *)
(* Goal: Z.le Z0 y *)
(* Goal: Z.le Z0 x *)
   rewrite (isnat_inj_abs y ny).
(* Goal: le (Z.abs_nat y) (Z.abs_nat x) *)
(* Goal: @eq Z y (Z.of_nat ny) *)
(* Goal: @eq Z x (Z.of_nat nx) *)
(* Goal: Z.le Z0 (Z.sub x y) *)
(* Goal: Z.le Z0 y *)
(* Goal: Z.le Z0 x *)
   apply lezle.
(* Goal: Z.lt Z0 x *)
   assumption.
(* Goal: Z.lt Z0 x *)
   assumption.
(* Goal: Z.le y x *)
(* Goal: Z.le Z0 y *)
(* Goal: Z.le Z0 x *)
   apply Zge_le.
(* Goal: Z.lt Z0 x *)
   assumption.
(* Goal: Z.lt Z0 x *)
   assumption.
(* Goal: Z.lt Z0 x *)
   assumption.
(* Goal: Z.le Z0 (Z.sub x y) *)
(* Goal: Z.le Z0 y *)
(* Goal: Z.le Z0 x *)
   unfold Zminus in |- *.
(* Goal: Z.le Z0 (Z.add x (Z.opp y)) *)
(* Goal: Z.le Z0 y *)
(* Goal: Z.le Z0 x *)
   apply Zle_left.
(* Goal: Z.le y x *)
(* Goal: Z.le Z0 y *)
(* Goal: Z.le Z0 x *)
   apply Zge_le.
(* Goal: Z.lt Z0 x *)
   assumption.
(* Goal: Z.lt Z0 x *)
   assumption.
(* Goal: Z.lt Z0 x *)
   assumption.
Qed.

Lemma abs_pred_pos :
 forall x : Z, (0 < x)%Z -> pred (Zabs_nat x) = Zabs_nat (x - 1).
Proof.
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intros.
(* Goal: @eq nat (Init.Nat.pred (Z.abs_nat x)) (Z.abs_nat (Z.sub x (Zpos xH))) *)
   rewrite abs_minus_pos.
(* Goal: @eq nat (Init.Nat.pred (Z.abs_nat x)) (Init.Nat.sub (Z.abs_nat x) (Z.abs_nat (Zpos xH))) *)
(* Goal: Z.le Z0 x *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.ge x (Zpos xH) *)
   replace (Zabs_nat 1) with 1.
(* Goal: @eq nat (Init.Nat.pred (Z.abs_nat x)) (Init.Nat.sub (Z.abs_nat x) (S O)) *)
(* Goal: @eq nat (S O) (Z.abs_nat (Zpos xH)) *)
(* Goal: Z.le Z0 x *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.ge x (Zpos xH) *)
   rewrite predminus1.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
(* Goal: @eq comparison Lt Lt *)
   reflexivity.
(* Goal: Z.le Z0 x *)
(* Goal: Z.le Z0 (Zpos xH) *)
(* Goal: Z.ge x (Zpos xH) *)
   apply Zlt_le_weak.
(* Goal: Z.lt Z0 x *)
   assumption.
(* Goal: Z.le Z0 (Zpos p) *)
(* Goal: Z.lt Z0 (Zpos p) *)
   unfold Zle in |- *.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *.
(* Goal: not (@eq comparison Eq Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   discriminate.
(* Goal: Z.ge x (Zpos xH) *)
   apply Zle_ge.
(* Goal: Z.le (Zpos xH) x *)
   change (Zsucc 0 <= x)%Z in |- *.
(* Goal: Z.le (Z.succ Z0) x *)
   apply Zlt_le_succ.
(* Goal: Z.lt Z0 x *)
   assumption.
Qed.

Lemma abs_neq_lt : forall x : Z, x <> 0%Z -> 0 < Zabs_nat x.
Proof.
(* Goal: forall (x : Z) (_ : not (@eq Z x Z0)), lt O (Z.abs_nat x) *)
   simple induction x.
(* Goal: @eq comparison Lt Lt *)
   intro. elim H. reflexivity.
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intros. change (Zabs_nat 0 < Zabs_nat (Zpos p)) in |- *. apply ltzlt.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   unfold Zle in |- *. simpl in |- *. discriminate.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   unfold Zle in |- *. simpl in |- *. discriminate.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   unfold Zlt in |- *. simpl in |- *. reflexivity.
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), lt O (Z.abs_nat (Zneg p)) *)
   intros. change (Zabs_nat 0 < Zabs_nat (Zpos p)) in |- *. apply ltzlt.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   unfold Zle in |- *. simpl in |- *. discriminate.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   unfold Zle in |- *. simpl in |- *. discriminate.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   unfold Zlt in |- *. simpl in |- *. reflexivity.
Qed.

Lemma nat_ge_0 : forall n : nat, (Z_of_nat n >= 0)%Z.
Proof.
(* Goal: forall n : nat, Z.ge (Z.of_nat n) Z0 *)
   simple induction n.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Lt) *)
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   simpl in |- *. unfold Zge in |- *. simpl in |- *. discriminate.
(* Goal: forall (n : nat) (_ : Z.ge (Z.of_nat n) Z0), Z.ge (Z.of_nat (S n)) Z0 *)
   intros m IHm.
(* Goal: Z.ge (Z.of_nat (S m)) Z0 *)
   change (Z_of_nat (S m) >= Z_of_nat 0)%Z in |- *.
(* Goal: Z.ge (Z.of_nat (S m)) (Z.of_nat O) *)
   apply Znat.inj_ge. unfold ge in |- *.
(* Goal: le O (S m) *)
   apply le_O_n.
Qed.
