(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA                        ENS-CNRS                *)
(*              Rocquencourt                        Lyon                    *)
(*                                                                          *)
(*                                Coq V5.10                                 *)
(*                              Nov 25th 1994                               *)
(*                                                                          *)
(****************************************************************************)
(*                                  Zle.v                                   *)
(****************************************************************************)
Require Export Arith.
Require Export misc.
Require Export groups.
Require Export Zbase.
Require Export Z_succ_pred.
Require Export Zadd.

(**************)
(* order on Z *)
(**************)

(************)
Definition leZ (x y : Z) :=
  match x return Prop with
  | OZ =>
      match y return Prop with
      | OZ => True
      | pos n => True
      | neg n => False
      end
  | pos n =>
      match y return Prop with
      | OZ => False
      | pos m => n <= m
      | neg m => False
      end
  | neg n =>
      match y return Prop with
      | OZ => True
      | pos m => True
      | neg m => m <= n
      end
  end.

(**************)
Lemma sign_absZ : forall x : Z, leZ OZ (absZ x).

Proof.
(* Goal: forall x : Z, leZ OZ (absZ x) *)
intros; elim x; simpl in |- *. exact I. intro; simpl in |- *. exact I. intro; simpl in |- *. exact I.
Qed.

(********************)
Lemma tech_le_pos_abs : forall x : Z, leZ OZ x -> absZ x = x.

Proof.
(* Goal: forall (x : Z) (_ : leZ OZ x), leZ (oppZ x) OZ *)
intros x; elim x. 
(* Goal: forall (n : nat) (_ : leZ OZ (pos n)), @eq Z (absZ (pos n)) (pos n) *)
(* Goal: forall (n : nat) (_ : leZ OZ (neg n)), @eq Z (absZ (neg n)) (neg n) *)
unfold absZ in |- *; reflexivity. unfold absZ in |- *; reflexivity. intros; elim H.
Qed.

(************************)
Theorem leZ_antisymmetric : antisym Z leZ.

Proof.
(* Goal: antisym Z leZ *)
unfold antisym in |- *; intros x y; elim x.
(* OZ *)
(* Goal: forall (_ : leZ OZ y) (_ : leZ y OZ), @eq Z OZ y *)
(* Goal: forall (n : nat) (_ : leZ (pos n) y) (_ : leZ y (pos n)), @eq Z (pos n) y *)
(* Goal: forall (n : nat) (_ : leZ (neg n) y) (_ : leZ y (neg n)), @eq Z (neg n) y *)
elim y.
(* OZ OZ *)
(* Goal: forall _ : lt_absZ OZ (pos O), @eq Z OZ OZ *)
(* Goal: forall (n : nat) (_ : lt_absZ (pos n) (pos O)), @eq Z (pos n) OZ *)
(* Goal: forall (n : nat) (_ : lt_absZ (neg n) (pos O)), @eq Z (neg n) OZ *)
reflexivity.
(* OZ (pos n) *)
(* Goal: forall (n0 : nat) (_ : leZ (neg n) (pos n0)) (_ : leZ (pos n0) (neg n)), @eq Z (neg n) (pos n0) *)
(* Goal: forall (n0 : nat) (_ : leZ (neg n) (neg n0)) (_ : leZ (neg n0) (neg n)), @eq Z (neg n) (neg n0) *)
intros; elim H0.
(* OZ (neg n) *)
(* Goal: forall (n : nat) (_ : leZ OZ (neg n)), leZ (oppZ (neg n)) OZ *)
intros; elim H.
(* (pos n) *)
(* Goal: forall (_ : leZ OZ y) (_ : leZ y OZ), @eq Z OZ y *)
(* Goal: forall (n : nat) (_ : leZ (pos n) y) (_ : leZ y (pos n)), @eq Z (pos n) y *)
(* Goal: forall (n : nat) (_ : leZ (neg n) y) (_ : leZ y (neg n)), @eq Z (neg n) y *)
intros n; elim y.
(* (pos n) OZ *)
(* Goal: forall (n : nat) (_ : leZ OZ (neg n)), leZ (oppZ (neg n)) OZ *)
intros; elim H.
(* (pos n) (pos n0) *)
(* Goal: forall _ : lt_absZ OZ (pos O), @eq Z OZ OZ *)
(* Goal: forall (n : nat) (_ : lt_absZ (pos n) (pos O)), @eq Z (pos n) OZ *)
(* Goal: forall (n : nat) (_ : lt_absZ (neg n) (pos O)), @eq Z (neg n) OZ *)
simpl in |- *; intros; elim (le_antisym n n0 H H0); reflexivity.
(* (pos n) (neg n0) *)
(* Goal: forall (n : nat) (_ : leZ OZ (neg n)), leZ (oppZ (neg n)) OZ *)
intros; elim H.
(* (neg n) *)
(* Goal: forall (_ : leZ OZ y) (_ : leZ y OZ), @eq Z OZ y *)
(* Goal: forall (n : nat) (_ : leZ (pos n) y) (_ : leZ y (pos n)), @eq Z (pos n) y *)
(* Goal: forall (n : nat) (_ : leZ (neg n) y) (_ : leZ y (neg n)), @eq Z (neg n) y *)
intros n; elim y.
(* (neg n) OZ *)
(* Goal: forall (n0 : nat) (_ : leZ (neg n) (pos n0)) (_ : leZ (pos n0) (neg n)), @eq Z (neg n) (pos n0) *)
(* Goal: forall (n0 : nat) (_ : leZ (neg n) (neg n0)) (_ : leZ (neg n0) (neg n)), @eq Z (neg n) (neg n0) *)
intros; elim H0.
(* (neg n) (pos n0) *)
(* Goal: forall (n0 : nat) (_ : leZ (neg n) (pos n0)) (_ : leZ (pos n0) (neg n)), @eq Z (neg n) (pos n0) *)
(* Goal: forall (n0 : nat) (_ : leZ (neg n) (neg n0)) (_ : leZ (neg n0) (neg n)), @eq Z (neg n) (neg n0) *)
intros; elim H0.
(* (neg n) (neg n0) *)
(* Goal: forall _ : lt_absZ OZ (pos O), @eq Z OZ OZ *)
(* Goal: forall (n : nat) (_ : lt_absZ (pos n) (pos O)), @eq Z (pos n) OZ *)
(* Goal: forall (n : nat) (_ : lt_absZ (neg n) (pos O)), @eq Z (neg n) OZ *)
simpl in |- *; intros; elim (le_antisym n0 n H H0); reflexivity.
Qed.

(************)
Definition ltZ (x y : Z) := leZ (succZ x) y.

(****************)
Definition lt_absZ (x y : Z) := ltZ (absZ x) (absZ y).

(*******************)
Lemma tech_lt_abs_OZ : forall x : Z, lt_absZ x (pos 0) -> x = OZ.

Proof.
(* Goal: forall (x : Z) (_ : lt_absZ x (pos O)), @eq Z x OZ *)
simple induction x.
(* OZ *)
(* Goal: forall _ : lt_absZ OZ (pos O), @eq Z OZ OZ *)
(* Goal: forall (n : nat) (_ : lt_absZ (pos n) (pos O)), @eq Z (pos n) OZ *)
(* Goal: forall (n : nat) (_ : lt_absZ (neg n) (pos O)), @eq Z (neg n) OZ *)
reflexivity.
(* pos n *)
unfold lt_absZ in |- *; unfold absZ in |- *; unfold ltZ in |- *;
(* Goal: forall (x y : Z) (_ : @eq Z x (oppZ y)) (_ : leZ OZ x) (_ : leZ OZ y), @eq Z x y *)
 unfold leZ in |- *; intros. 
(* Goal: @eq Z (neg n) OZ *)
elim (le_Sn_O n H).
(* neg n *)
unfold lt_absZ in |- *; unfold absZ in |- *; unfold ltZ in |- *;
(* Goal: forall (x y : Z) (_ : @eq Z x (oppZ y)) (_ : leZ OZ x) (_ : leZ OZ y), @eq Z x y *)
 unfold leZ in |- *; intros. 
(* Goal: @eq Z (neg n) OZ *)
elim (le_Sn_O n H).
Qed.

(*******************)
Lemma tech_posOZ_pos : forall n : nat, leZ OZ (posOZ n).

Proof.
(* Goal: True *)
intros; elim n. simpl in |- *; exact I. simpl in |- *; intros; exact I.
Qed.

(**************)
Lemma le_opp_OZ_l : forall x : Z, leZ OZ x -> leZ (oppZ x) OZ.

Proof.
(* Goal: True *)
intros x; elim x. simpl in |- *; intros; exact I. simpl in |- *; intros; exact I. 
(* Goal: forall (n : nat) (_ : leZ OZ (neg n)), leZ (oppZ (neg n)) OZ *)
intros; elim H.
Qed.

(**************)
Lemma le_opp_OZ :
 forall x y : Z, x = oppZ y -> leZ OZ x -> leZ OZ y -> x = OZ.

Proof.
(* Goal: forall (x y : Z) (_ : @eq Z x (oppZ y)) (_ : leZ OZ x) (_ : leZ OZ y), @eq Z x y *)
intros. apply (leZ_antisymmetric x OZ). rewrite H. exact (le_opp_OZ_l y H1).
(* Goal: leZ OZ x *)
exact H0.
Qed.

(***************)
Lemma le_opp_OZ2 :
 forall x y : Z, x = oppZ y -> leZ OZ x -> leZ OZ y -> x = y.

Proof.
(* Goal: forall (x y : Z) (_ : @eq Z x (oppZ y)) (_ : leZ OZ x) (_ : leZ OZ y), @eq Z x y *)
intros.
(* Goal: @eq Z x y *)
rewrite (le_opp_OZ x y H H0 H1). 
(* Goal: @eq Z OZ y *)
rewrite (opp_opp Z IdZ addZ OZ oppZ Z_group y I); elim H.
(* Goal: forall _ : lt_absZ OZ (pos O), @eq Z OZ OZ *)
(* Goal: forall (n : nat) (_ : lt_absZ (pos n) (pos O)), @eq Z (pos n) OZ *)
(* Goal: forall (n : nat) (_ : lt_absZ (neg n) (pos O)), @eq Z (neg n) OZ *)
rewrite (le_opp_OZ x y H H0 H1); simpl in |- *; reflexivity.
Qed.
