Faux.v

(****************************************************************************                                                                                         IEEE754  :  Faux                                                                                                                                            Laurent Thery                                                                                                                                     ***************************************************************************** Auxillary properties about natural numbers, relative numbers and reals *)
Require Import Min.
Require Import Arith.
Require Import Reals.
Require Import Zpower.
Require Import fast_integer.
Require Import sTactic.
Hints Resolve R1_neq_R0 :real.
(*Missing rule for nat *)

Theorem minus_minus: (a, b:nat) (le a b) ->(minus b (minus b a))=a.
Intros a b H'.
Apply sym_equal.
Apply plus_minus; Auto.
Rewrite plus_sym; Apply le_plus_minus; Auto.
Qed.

Theorem lte_comp_mult:
  (p, q, r, t:nat) (le p q) -> (le r t) ->(le (mult p r) (mult q t)).
Intros p q r t H'; Elim H'; Simpl; Auto with arith.
Elim p; Simpl; Auto with arith.
Intros n0 H'0 H'1; Apply le_plus_plus; Auto.
Intros m H'0 H'1 H'2.
Apply le_trans with m := (mult m t); Auto with arith.
Qed.
Hints Resolve lte_comp_mult :arith.

Theorem le_refl_eq: (n, m:nat) n=m ->(le n m).
Intros n m H'; Rewrite H'; Auto.
Qed.

Theorem lt_le_pred: (n, m:nat) (lt n m) ->(le n (pred m)).
Intros n m H'; Inversion H'; Simpl; Auto.
Apply le_trans with (S n); Auto.
Qed.

Theorem lt_comp_mult_l:
  (p, q, r:nat) (lt O p) -> (lt q r) ->(lt (mult p q) (mult p r)).
Intros p; Elim p; Simpl.
Auto with arith.
Intros n0; Case n0.
Simpl; Auto with arith.
Intros n1 H' q r H'0 H'1.
Apply lt_trans with m := (plus q (mult (S n1) r)); Auto with arith.
Qed.
Hints Resolve lt_comp_mult_l :arith.

Theorem lt_comp_mult_r:
  (p, q, r:nat) (lt O p) -> (lt q r) ->(lt (mult q p) (mult r p)).
Intros; Repeat Rewrite [x:nat](mult_sym x p); Auto with arith.
Qed.
Hints Resolve lt_comp_mult_r :arith.

Theorem lt_comp_mult:
  (p, q, r, s:nat) (lt p q) -> (lt r s) ->(lt (mult p r) (mult q s)).
Intros p q r s; Case q.
Intros H'; Inversion H'.
Intros q'; Case p.
Intros H' H'0; Simpl; Apply le_lt_trans with m := r; Auto with arith.
Intros p' H' H'0; Apply le_lt_trans with m := (mult (S q') r); Auto with arith.
Qed.
Hints Resolve lt_comp_mult :arith.

Theorem mult_eq_inv: (n, m, p:nat) (lt O n) -> (mult n m)=(mult n p) ->m=p.
Intros n m p H' H'0.
Apply le_antisym; Auto.
Case (le_or_lt m p); Intros H'1; Auto with arith.
Absurd (lt (mult n p) (mult n m)); Auto with arith.
Rewrite H'0; Auto with arith.
Case (le_or_lt p m); Intros H'1; Auto with arith.
Absurd (lt (mult n m) (mult n p)); Auto with arith.
Rewrite H'0; Auto with arith.
Qed.

Definition natEq: (n, m:nat){n=m}+{~ n=m}.
Intros n; Elim n.
Intros m; Case m; Auto with arith.
Intros n0 H' m; Case m; Auto with arith.
Intros n1.
Case (H' n1); Auto with arith.
Defined.

Theorem notEqLt: (n:nat) (lt O n) ->~ n=O.
Intros n H'; Contradict H'; Auto.
Rewrite H'; Auto with arith.
Qed.
Hints Resolve notEqLt :arith.

Theorem lt_next: (n, m:nat) (lt n m) ->m=(S n) \/ (lt (S n) m).
Intros n m H'; Elim H'; Auto with arith.
Qed.

Theorem le_next: (n, m:nat) (le n m) ->m=n \/ (le (S n) m).
Intros n m H'; Case (le_lt_or_eq ? ? H'); Auto with arith.
Qed.

Theorem min_or: (n, m:nat)(min n m)=n /\ (le n m) \/ (min n m)=m /\ (lt m n).
Intros n; Elim n; Simpl; Auto with arith.
Intros n' Rec m; Case m; Simpl; Auto with arith.
Intros m'; Elim (Rec m'); Intros H'0; Case H'0; Clear H'0; Intros H'0 H'1;
Rewrite H'0; Auto with arith.
Qed.

Theorem minus_inv_lt_aux: (n, m:nat) (minus n m)=O ->(minus n (S m))=O.
Intros n; Elim n; Simpl; Auto with arith.
Intros n0 H' m; Case m; Auto with arith.
Intros H'0; Discriminate.
Qed.

Theorem minus_inv_lt: (n, m:nat) (le m n) ->(minus m n)=O.
Intros n m H'; Elim H'; Simpl; Auto with arith.
Intros m0 H'0 H'1; Apply minus_inv_lt_aux; Auto.
Qed.

Theorem minus_le:
  (m, n, p, q:nat) (le m n) -> (le p q) ->(le (minus m q) (minus n p)).
Intros m n p q H' H'0.
Case (le_or_lt m q); Intros H'1.
Rewrite minus_inv_lt with 1 := H'1; Auto with arith.
Apply simpl_le_plus_l with p := q.
Rewrite le_plus_minus_r; Auto with arith.
Rewrite (le_plus_minus p q); Auto.
Rewrite (plus_sym p).
Rewrite plus_assoc_r.
Rewrite le_plus_minus_r; Auto with arith.
Apply le_trans with 1 := H'; Auto with arith.
Apply le_trans with 1 := H'0; Auto with arith.
Apply le_trans with 2 := H'; Auto with arith.
Qed.

Theorem lt_mult_anti_compatibility:
  (n, n1, n2:nat) (lt O n) -> (lt (mult n n1) (mult n n2)) ->(lt n1 n2).
Intros n n1 n2 H' H'0; Case (le_or_lt n2 n1); Auto.
Intros H'1; Contradict H'0; Auto.
Apply le_not_lt; Auto with arith.
Qed.

Theorem le_mult_anti_compatibility:
  (n, n1, n2:nat) (lt O n) -> (le (mult n n1) (mult n n2)) ->(le n1 n2).
Intros n n1 n2 H' H'0; Case (le_or_lt n1 n2); Auto.
Intros H'1; Contradict H'0; Auto.
Apply lt_not_le; Auto with arith.
Qed.

Theorem min_n_0: (n:nat)(min n O)=O.
Intros n; Case n; Simpl; Auto.
Qed.
(*Simplification rules missing in R *)

Theorem Rplus_ne_l: (r:R)(Rplus r R0)==r.
Intros r; Case (Rplus_ne r); Auto.
Qed.

Theorem Rplus_ne_r: (r:R)(Rplus R0 r)==r.
Intros r; Case (Rplus_ne r); Auto.
Qed.

Theorem Rmult_ne_l: (r:R)(Rmult r R1)==r.
Intros r; Case (Rmult_ne r); Auto.
Qed.

Theorem Rmult_ne_r: (r:R)(Rmult R1 r)==r.
Intros r; Case (Rmult_ne r); Auto.
Qed.
Hints Resolve Rplus_ne_l Rplus_ne_r Rmult_ne_l Rmult_ne_r :real.

Theorem Rminus_Ropp: (x, y:R)(Ropp (Rminus y x))==(Rminus x y).
Intros; Ring.
Qed.

Theorem Rle_ref: (x:R)(Rle x x).
Intros x; Apply eq_Rle; Auto with real.
Qed.
Hints Resolve Rle_ref :real.

Theorem Rle_monotony:
  (r, r1, r2:R) (Rle R0 r) -> (Rle r1 r2) ->(Rle (Rmult r r1) (Rmult r r2)).
Intros r r1 r2 H' H'0.
Case H'; Intros H'1.
Case H'0; Intros H'1; Auto with real.
Apply Rlt_le; Apply Rlt_monotony; Auto with real.
Rewrite H'2; Auto with real.
Rewrite <- H'1; Repeat Rewrite Rmult_Ol; Auto with real.
Qed.
Hints Resolve Rlt_monotony Rle_monotony :real.

Theorem Rle_monotony_r:
  (r, r1, r2:R) (Rle R0 r) -> (Rle r1 r2) ->(Rle (Rmult r1 r) (Rmult r2 r)).
Intros r r1 r2 H' H'0; Repeat Rewrite [x:R](Rmult_sym x r); Auto with real.
Qed.

Theorem Rlt_monotony_r:
  (r, r1, r2:R) (Rlt R0 r) -> (Rlt r1 r2) ->(Rlt (Rmult r1 r) (Rmult r2 r)).
Intros r r1 r2 H' H'0; Repeat Rewrite [x:R](Rmult_sym x r); Auto with real.
Qed.
Hints Resolve Rlt_monotony Rle_monotony :real.

Theorem Rle_Rmult_comp:
  (x, y, z, t:R) (Rle R0 x) -> (Rle R0 z) -> (Rle x y) -> (Rle z t) ->
  (Rle (Rmult x z) (Rmult y t)).
Intros x y z t H' H'0 H'1 H'2.
Apply Rle_trans with r2 := (Rmult x t); Auto with real.
Repeat Rewrite [x:?](Rmult_sym x t).
Apply Rle_monotony; Auto.
Apply Rle_trans with z; Auto.
Qed.
Hints Resolve Rle_Rmult_comp :real.

Theorem Rlt_Ropp: (x, y:R) (Rlt y x) ->(Rlt (Ropp x) (Ropp y)).
Intros x y H'.
Apply Rgt_Ropp; Auto.
Qed.
Hints Resolve Rlt_Ropp :real.

Theorem Ropp_Rlt: (x, y:R) (Rlt (Ropp y) (Ropp x)) ->(Rlt x y).
Intros x y H'.
Rewrite <- (Ropp_Ropp x); Rewrite <- (Ropp_Ropp y); Auto with real.
Qed.

Theorem Rle_Ropp: (x, y:R) (Rle y x) ->(Rle (Ropp x) (Ropp y)).
Intros x y H'.
Case H'; Clear H'; Intros H'; Auto with real.
Apply Rlt_le; Auto with real.
Apply eq_Rle; Auto with real.
Qed.
Hints Resolve Rle_Ropp :real.

Theorem Ropp_Rle: (x, y:R) (Rle (Ropp y) (Ropp x)) ->(Rle x y).
Intros x y H'.
Rewrite <- (Ropp_Ropp x); Rewrite <- (Ropp_Ropp y); Auto with real.
Qed.

Theorem Rplus_Rminus: (p, q:R)(Rplus p (Rminus q p))==q.
Intros p q; Unfold Rminus.
Rewrite (Rplus_sym q); Rewrite <- Rplus_assoc; Auto with real.
Rewrite Rplus_Ropp_r; Auto with real.
Qed.
Hints Resolve Rplus_Ropp_r Rplus_Rminus Rlt_R0_R1 :real.

Theorem Rinv_RN: (e:R) ~ e==R0 ->~ (Rinv e)==R0.
Intros e H'; Red; Intros H'0; Absurd R1==R0; Auto with real.
Rewrite <- (Rinv_l e); Auto with real; Rewrite H'0; Auto with real.
Qed.
Hints Resolve Rinv_RN :real.

Theorem Rinv_Rinv: (e:R) ~ e==R0 ->(Rinv (Rinv e))==e.
Intros e H'; Apply r_Rmult_mult with r := (Rinv e); Auto with real.
Rewrite (Rmult_sym (Rinv e)); Repeat Rewrite Rinv_l; Auto with real.
Qed.
Hints Resolve Rinv_Rinv :real.

Theorem Rmult_Rminus_distr:
  (r1, r2, r3:R)(Rmult r1 (Rminus r2 r3))==(Rminus (Rmult r1 r2) (Rmult r1 r3)).
Intros r1 r2 r3; Unfold Rminus; Rewrite Rmult_Rplus_distr; Auto with real.
Apply Rplus_plus_r.
Rewrite <- (Ropp_Ropp r1).
Rewrite Ropp_mul2; Rewrite Ropp_mul1.
Rewrite Ropp_Ropp; Auto with real.
Qed.

Theorem Rle_or_lt: (n, m:R)(Rle n m) \/ (Rlt m n).
Intros n m; Case (total_order n m); Intros H'; Auto with real.
Left; Apply Rlt_le; Auto with real.
Elim H'; Clear H'; Intros H'; Try Rewrite H'; Auto with real.
Qed.

Theorem le_IZR: (p, q:Z) (Rle (IZR p) (IZR q)) ->(Zle p q).
Intros p q H'; Case H'; Auto.
Intros H'0; Apply Zlt_le_weak.
Apply lt_IZR; Auto.
Intros H'0; Rewrite (eq_IZR ? ? H'0); Auto with zarith.
Qed.
Hints Resolve Rle_not Rlt_antirefl Rlt_antisym :real.

Theorem Rlt_not: (r1, r2:R) (Rle r2 r1) ->~ (Rlt r1 r2).
Intros r1 r2 H'; Contradict H'; Auto with real.
Qed.

Theorem Rlt_mult_anticompatibility:
  (x, y, z:R) (Rlt (Rmult z x) (Rmult z y)) -> (Rlt R0 z) ->(Rlt x y).
Intros x y z H' H'0.
Case (total_order x y); Intros Eq0; Auto; Case Eq0; Clear Eq0; Intros Eq0;
Contradict H'; Auto with real.
Rewrite <- Eq0; Apply Rlt_antirefl; Auto with real.
Qed.

Theorem Rle_mult_anticompatibility:
  (x, y, z:R) (Rle (Rmult z x) (Rmult z y)) -> (Rlt R0 z) ->(Rle x y).
Intros x y z H' H'0; Case H'; Auto with real.
Intros H'1; Apply Rlt_le.
Apply Rlt_mult_anticompatibility with z := z; Auto.
Intros H'1.
Replace x with (Rmult (Rinv z) (Rmult z x)); Auto with real.
Replace y with (Rmult (Rinv z) (Rmult z y)); Auto with real.
Rewrite H'1; Auto with real.
Rewrite <- Rmult_assoc; Auto with real.
Rewrite Rinv_l; Auto with real.
Apply imp_not_Req; Auto.
Rewrite <- Rmult_assoc; Auto with real.
Rewrite Rinv_l; Auto with real.
Apply imp_not_Req; Auto.
Qed.

Theorem Rmult_anticompatibility:
  (r1, r2, r3:R) ~ r1==R0 -> (Rmult r1 r2)==(Rmult r1 r3) ->r2==r3.
Intros r1 r2 r3 H' H'0.
Replace r2 with (Rmult (Rinv r1) (Rmult r1 r2)).
Rewrite H'0.
Rewrite <- Rmult_assoc; Rewrite Rinv_l; Auto.
Ring.
Rewrite <- Rmult_assoc; Rewrite Rinv_l; Auto.
Ring.
Qed.

Theorem Rlt_Rinv_R1: (x, y:R) (Rle R1 x) -> (Rlt x y) ->(Rlt (Rinv y) (Rinv x)).
Intros x y H' H'0.
Cut (Rlt R0 x); [Intros Lt0 | Apply Rlt_le_trans with r2 := R1]; Auto with real.
Apply Rlt_mult_anticompatibility with z := x; Auto with real.
Rewrite (Rmult_sym x (Rinv x)); Rewrite Rinv_l; Auto with real.
2:Apply imp_not_Req; Auto.
Apply Rlt_mult_anticompatibility with z := y; Auto with real.
Rewrite (Rmult_sym x); Rewrite <- Rmult_assoc; Rewrite (Rmult_sym y (Rinv y));
Rewrite Rinv_l; Auto with real.
Rewrite Rmult_ne_l; Rewrite Rmult_ne_r; Auto.
Apply imp_not_Req; Right.
Red; Apply Rlt_trans with r2 := x; Auto with real.
Apply Rlt_trans with r2 := x; Auto with real.
Qed.
Hints Resolve Rlt_Rinv_R1 :reals.

Theorem R1_Rinv: (Rinv R1)==R1.
Apply trans_eqT with y := (Rmult (Rinv R1) R1); Auto with real.
Apply Rinv_l.
Exact R1_neq_R0.
Qed.
Hints Resolve R1_Rinv :real.

Theorem Rabsolu_R1: (Rabsolu R1)==R1.
Unfold Rabsolu; Case (case_Rabsolu R1); Auto with real.
Intros H'; Contradict H'; Auto with real.
Qed.
Hints Resolve Rabsolu_R1 :real.

Theorem Rle_antisym: (r, s:R) (Rle r s) -> (Rle s r) ->r==s.
Intros r s H' H'0.
Case (Rle_le_eq r s); Auto.
Qed.

Theorem RabsoluR0Inv: (r:R) (Rle (Rabsolu r) R0) ->r==R0.
Intros r; Unfold Rabsolu; Case (case_Rabsolu r).
Intros H' H'0; Contradict H'0; Apply Rle_not.
Replace R0 with (Ropp R0); Auto with real.
Intros H' H'0; Apply Rle_antisym; Auto with real.
Apply Rle_sym2; Auto.
Qed.

Theorem Rminus_Rabsolu:
  (p, q:R) (Rle q p) ->(Rabsolu (Rminus p q))==(Rminus p q).
Intros p q H'; Unfold Rabsolu.
Case (case_Rabsolu (Rminus p q)); Auto.
Intros H'0; Contradict H'; Auto with real.
Apply Rle_not; Auto with real.
Apply Rminus_lt; Auto.
Qed.

Theorem Rabsolu_Ropp: (r:R)(Rabsolu (Ropp r))==(Rabsolu r).
Intros r; Unfold Rabsolu.
Case (case_Rabsolu (Ropp r)); Case (case_Rabsolu r); Auto with real.
Intros H' H'0; Contradict H'0; Replace R0 with (Ropp R0); Auto with real.
Rewrite Ropp_Ropp; Auto.
Intros H' H'0; Apply trans_eqT with R0.
Apply Rle_antisym; Auto with real.
Replace R0 with (Ropp R0); Auto with real.
Apply Rle_Ropp; Apply Rle_sym2; Auto.
Apply Rle_sym2; Auto.
Apply Rle_antisym; Auto with real.
Apply Rle_sym2; Auto.
Apply Ropp_Rle; Rewrite Ropp_O; Apply Rle_sym2; Auto.
Qed.

Theorem Rabsolu_simpl1: (x:R) (Rle R0 x) ->(Rabsolu x)==x.
Intros x H'; Unfold Rabsolu.
Case (case_Rabsolu x); Auto.
Intros H'0; Contradict H'0; Auto with real.
Apply Rlt_not; Auto.
Qed.

Theorem Rabsolu_simpl2: (x:R) (Rle x R0) ->(Rabsolu x)==(Ropp x).
Intros x H'; Unfold Rabsolu.
Case (case_Rabsolu x); Auto.
Case H'; Intros H'1.
Intros H'0; Contradict H'1; Auto with real.
Apply Rlt_not; Auto with real.
Apply Rle_sym2; Auto.
Rewrite H'1; Auto with real.
Qed.

Theorem RabsoluR0: (r:R)(Rle R0 (Rabsolu r)).
Intros r; Unfold Rabsolu; Case (case_Rabsolu r).
Intros H'; Apply Rlt_le; Replace R0 with (Ropp R0); Auto with real.
Intros H'; Apply Rle_sym2; Auto.
Qed.
Hints Resolve RabsoluR0 :real.

Theorem Rabsolu_Rabsolu: (r:R)(Rabsolu (Rabsolu r))==(Rabsolu r).
Intros r; Apply Rabsolu_simpl1; Auto with real.
Qed.

Theorem Rplus_le:
  (r1, r2, r3, r4:R) (Rle r1 r2) -> (Rle r3 r4) ->
  (Rle (Rplus r1 r3) (Rplus r2 r4)).
Intros r1 r2 r3 r4 H' H'0; Apply Rle_trans with (Rplus r1 r4); Auto with real.
Apply Rle_compatibility; Auto.
Repeat Rewrite [x:R](Rplus_sym x r4).
Apply Rle_compatibility; Auto.
Qed.
Hints Resolve Rplus_le :real.

Definition Rmax: R -> R ->R :=
   [x, y:R]
      Cases (total_order_Rle x y) of
          (leftT _) => y
         | (rightT _) => x
      end.

Theorem RmaxLess1: (r1, r2:R)(Rle r1 (Rmax r1 r2)).
Intros r1 r2; Unfold Rmax; Case (total_order_Rle r1 r2); Auto with real.
Qed.

Theorem RmaxLess2: (r1, r2:R)(Rle r2 (Rmax r1 r2)).
Intros r1 r2; Unfold Rmax; Case (total_order_Rle r1 r2); Auto with real.
Intros H'; Case (Rle_or_lt r2 r1); Auto.
Intros H'0; Contradict H'; Apply Rlt_le; Auto.
Qed.

Theorem RmaxSym: (p, q:R)(Rmax p q)==(Rmax q p).
Intros p q; Unfold Rmax.
Case (total_order_Rle p q); Case (total_order_Rle q p); Auto; Intros H1 H2;
Apply Rle_antisym; Auto.
Case (Rle_or_lt p q); Auto; Intros H'0; Contradict H1; Apply Rlt_le; Auto.
Case (Rle_or_lt q p); Auto; Intros H'0; Contradict H2; Apply Rlt_le; Auto.
Qed.

Theorem RmaxAbs:
  (p, q, r:R) (Rle p q) -> (Rle q r) ->
  (Rle (Rabsolu q) (Rmax (Rabsolu p) (Rabsolu r))).
Intros p q r H' H'0; Case (Rle_or_lt R0 p); Intros H'1.
Repeat Rewrite Rabsolu_simpl1; Auto.
Apply Rle_trans with r; Auto.
Apply RmaxLess2; Auto.
Apply Rle_trans with p; Auto; Apply Rle_trans with q; Auto.
Apply Rle_trans with p; Auto.
Rewrite (Rabsolu_simpl2 p); [Idtac | Apply Rlt_le; Auto].
Case (Rle_or_lt R0 q); Intros H'2.
Repeat Rewrite Rabsolu_simpl1; Auto.
Apply Rle_trans with r; Auto.
Apply RmaxLess2; Auto.
Apply Rle_trans with q; Auto.
Rewrite (Rabsolu_simpl2 q); [Idtac | Apply Rlt_le; Auto].
Case (Rle_or_lt R0 r); Intros H'3.
Repeat Rewrite Rabsolu_simpl1; Auto.
Apply Rle_trans with (Ropp p); Auto with real.
Apply RmaxLess1; Auto.
Rewrite (Rabsolu_simpl2 r); [Idtac | Apply Rlt_le; Auto].
Apply Rle_trans with (Ropp p); Auto with real.
Apply RmaxLess1; Auto.
Qed.

Theorem RmaxRmult:
  (p, q, r:R) (Rle R0 r) ->(Rmax (Rmult r p) (Rmult r q))==(Rmult r (Rmax p q)).
Intros p q r H; Unfold Rmax.
Case (total_order_Rle p q); Case (total_order_Rle (Rmult r p) (Rmult r q));
Auto; Intros H1 H2; Auto.
Case H; Intros E1.
Case H1; Auto with real.
Rewrite <- E1; Repeat Rewrite Rmult_Ol; Auto.
Case H; Intros E1.
Case H2; Auto with real.
Apply Rle_mult_anticompatibility with z := r; Auto.
Rewrite <- E1; Repeat Rewrite Rmult_Ol; Auto.
Qed.
(* Properties of Z *)

Theorem convert_not_O: (p:positive)~ (convert p)=O.
Intros p; Elim p.
Intros p0 H'; Unfold convert; Simpl; Rewrite ZL6.
Generalize H'; Case (convert p0); Auto.
Intros p0 H'; Unfold convert; Simpl; Rewrite ZL6.
Generalize H'; Case (convert p0); Simpl; Auto.
Unfold convert; Simpl; Auto with arith.
Qed.
Hints Resolve convert_not_O :zarith arith.
Hints Resolve
Zlt_le_weak Zle_not_gt Zgt_antirefl Zlt_n_n Zle_not_lt Zlt_not_le Zlt_not_sym
inj_lt inj_le :zarith.

Theorem inj_abs: (x:Z) (Zle ZERO x) ->(inject_nat (absolu x))=x.
Intros x; Elim x; Auto.
Unfold absolu.
Intros p.
Pattern 1 3 p; Rewrite <- (bij3 p).
Generalize (convert_not_O p); Case (convert p); Simpl; Auto with arith.
Intros H'; Case H'; Auto.
Intros n H' H'0; Rewrite sub_add_one; Auto.
Intros p H'; Contradict H'; Auto.
Qed.

Theorem inject_nat_convert:
  (p:Z) (q:positive) p=(POS q) ->(inject_nat (convert q))=p.
Intros p q H'; Rewrite H'.
CaseEq (convert q); Simpl.
Elim q; Unfold convert; Simpl; Intros; Try Discriminate.
Absurd ZERO=(POS p0); Auto.
Red; Intros H'0; Try Discriminate.
Apply H; Auto.
Change (convert p0)=O.
Generalize H0; Rewrite ZL6; Case (convert p0); Simpl; Auto; Intros;
Try Discriminate.
Intros n; Rewrite <- bij1.
Intros H'0; Apply f_equal with f := POS.
Apply convert_intro; Auto.
Qed.
Hints Resolve inj_le inj_lt :zarith.

Theorem ZleLe: (x, y:nat) (Zle (INZ x) (INZ y)) ->(le x y).
Intros x y H'.
Case (le_or_lt x y); Auto with arith.
Intros H'0; Contradict H'; Auto with zarith.
Qed.

Theorem inject_nat_eq: (x, y:nat) (inject_nat x)=(inject_nat y) ->x=y.
Intros x y H'; Apply le_antisym.
Apply ZleLe; Auto.
Unfold INZ; Rewrite H'; Auto with zarith.
Apply ZleLe; Auto.
Unfold INZ; Rewrite H'; Auto with zarith.
Qed.

Theorem Zcompare_EGAL: (p, q:Z) (Zcompare p q)=EGAL ->p=q.
Intros p q; Case p; Case q; Simpl; Auto with arith; Try (Intros; Discriminate);
Intros q1 p1.
Intros H1; Rewrite (compare_convert_EGAL p1 q1); Auto.
Generalize (compare_convert_EGAL p1 q1); Case (compare p1 q1 EGAL); Simpl;
Intros H H1; Try Discriminate; Rewrite H; Auto.
Qed.

Theorem Zlt_Zopp: (x, y:Z) (Zlt x y) ->(Zlt (Zopp y) (Zopp x)).
Intros x y; Case x; Case y; Simpl; Auto with zarith; Intros p p0; Unfold Zlt;
Simpl; Rewrite <- ZC4; Auto.
Qed.
Hints Resolve Zlt_Zopp :zarith.

Theorem Zle_Zopp: (x, y:Z) (Zle x y) ->(Zle (Zopp y) (Zopp x)).
Intros x y H'; Case (Zle_lt_or_eq ? ? H'); Auto with zarith.
Intros H'0; Rewrite H'0; Auto with zarith.
Qed.
Hints Resolve Zle_Zopp :zarith.

Theorem absolu_INR: (n:nat)(absolu (inject_nat n))=n.
Intros n; Case n; Simpl; Auto with arith.
Intros n0; Rewrite bij1; Auto with arith.
Qed.

Theorem absolu_Zopp: (p:Z)(absolu (Zopp p))=(absolu p).
Intros p; Case p; Simpl; Auto.
Qed.

Theorem Zabs_absolu: (z:Z)(Zabs z)=(inject_nat (absolu z)).
Intros z; Case z; Simpl; Auto; Intros p; Apply sym_equal;
Apply inject_nat_convert; Auto.
Qed.

Theorem absolu_comp_mult:
  (p, q:Z)(absolu (Zmult p q))=(mult (absolu p) (absolu q)).
Intros p q; Case p; Case q; Simpl; Auto; Intros p0 p1;
Apply (times1_convert p1 p0 [x:?]x).
Qed.

Theorem Zmin_sym: (m, n:Z)(Zmin n m)=(Zmin m n).
Intros m n; Unfold Zmin.
Case n; Case m; Simpl; Auto.
Intros p p0; Rewrite (ZC4 p p0).
Generalize (compare_convert_EGAL p0 p).
Case (compare p0 p EGAL); Simpl; Auto.
Intros H'; Rewrite H'; Auto.
Intros p p0; Rewrite (ZC4 p p0).
Generalize (compare_convert_EGAL p0 p).
Case (compare p0 p EGAL); Simpl; Auto.
Intros H'; Rewrite H'; Auto.
Qed.

Theorem Zpower_nat_O: (z:Z)(Zpower_nat z O)=(inject_nat (S O)).
Intros z; Unfold Zpower_nat; Simpl; Auto.
Qed.

Theorem Zpower_nat_1: (z:Z)(Zpower_nat z (S O))=z.
Intros z; Unfold Zpower_nat; Simpl; Rewrite Zmult_n_1; Auto.
Qed.

Theorem Zmin_le1: (z1, z2:Z) (Zle z1 z2) ->(Zmin z1 z2)=z1.
Intros z1 z2; Unfold Zle Zmin; Case (Zcompare z1 z2); Auto; Intros H;
Contradict H; Auto.
Qed.

Theorem Zmin_le2: (z1, z2:Z) (Zle z2 z1) ->(Zmin z1 z2)=z2.
Intros z1 z2 H; Rewrite Zmin_sym; Apply Zmin_le1; Auto.
Qed.

Theorem Zminus_n_predm: (n, m:Z)(Zs (Zminus n m))=(Zminus n (Zpred m)).
Intros n m.
Unfold Zpred; Unfold Zs; Ring.
Qed.

Theorem Zopp_Zpred_Zs: (z:Z)(Zopp (Zpred z))=(Zs (Zopp z)).
Intros z; Unfold Zpred Zs; Ring.
Qed.

Theorem Zle_mult_gen:
  (x, y:Z) (Zle ZERO x) -> (Zle ZERO y) ->(Zle ZERO (Zmult x y)).
Intros x y H' H'0; Case (Zle_lt_or_eq ? ? H').
Intros H'1; Rewrite Zmult_sym; Apply Zle_mult; Auto; Apply Zlt_gt; Auto.
Intros H'1; Rewrite <- H'1; Simpl; Auto with zarith.
Qed.
Hints Resolve Zle_mult_gen :zarith.

Definition Zmax: (_, _:Z)Z :=
   [n, m:Z]
      Cases (Zcompare n m) of
          EGAL => m
         | INFERIEUR => m
         | SUPERIEUR => n
      end.

Theorem ZmaxLe1: (z1, z2:Z)(Zle z1 (Zmax z1 z2)).
Intros z1 z2; Unfold Zmax; CaseEq (Zcompare z1 z2); Simpl; Auto with zarith.
Unfold Zle; Intros H; Rewrite H; Red; Intros; Discriminate.
Qed.

Theorem ZmaxSym: (z1, z2:Z)(Zmax z1 z2)=(Zmax z2 z1).
Intros z1 z2; Unfold Zmax; CaseEq (Zcompare z1 z2); CaseEq (Zcompare z2 z1);
Intros H1 H2; Try Case (Zcompare_EGAL ? ? H1); Auto;
Try Case (Zcompare_EGAL ? ? H2); Auto; Contradict H1.
Case (Zcompare_ANTISYM z2 z1); Auto.
Intros H' H'0; Rewrite H'0; Auto; Red; Intros; Discriminate.
Case (Zcompare_ANTISYM z1 z2); Auto.
Intros H'; Rewrite H'; Auto; Intros; Red; Intros; Discriminate.
Qed.

Theorem ZmaxLe2: (z1, z2:Z)(Zle z2 (Zmax z1 z2)).
Intros z1 z2; Rewrite ZmaxSym; Apply ZmaxLe1.
Qed.
Hints Resolve ZmaxLe1 ZmaxLe2 :zarith.
(* Conversions from R <-> Z  <-> N *)

Theorem IZR_zero: (p:Z) p=ZERO ->(IZR p)==R0.
Intros p H'; Rewrite H'; Auto.
Qed.
Hints Resolve not_O_INR :real.

Theorem IZR_zero_r: (p:Z) (IZR p)==R0 ->p=ZERO.
Intros p; Case p; Simpl; Auto.
Intros p1 H'; Contradict H'; Auto with real zarith.
Intros p1 H'; Absurd (INR (convert p1))==R0; Auto with real zarith.
Rewrite <- (Ropp_Ropp (INR (convert p1))).
Rewrite H'; Auto with real.
Qed.

Theorem Rminus_IZR: (z, t:Z)(IZR (Zminus z t))==(Rminus (IZR z) (IZR t)).
Intros z t; Unfold Rminus; Rewrite <- Ropp_Ropp_IZR; Rewrite <- plus_IZR; Auto.
Qed.

Theorem Rlt_INR: (n, m:nat) (lt n m) ->(Rlt (INR n) (INR m)).
Intros n m H'; Elim H'; Auto.
Replace (INR n) with (Rplus (INR n) R0); Auto with real; Rewrite S_INR;
Auto with real.
Apply Rlt_compatibility; Auto with real.
Intros m0 H'0 H'1.
Replace (INR n) with (Rplus (INR n) R0); Auto with real; Rewrite S_INR;
Auto with real.
Apply Rplus_lt; Auto with real.
Qed.
Hints Resolve Rlt_INR :real.

Theorem Rlt_INR0: (n:nat) (lt O n) ->(Rlt R0 (INR n)).
Replace R0 with (INR O); Auto with real.
Qed.
Hints Resolve Rlt_INR0 :real.

Theorem Rlt_INR1: (n:nat) (lt (S O) n) ->(Rlt R1 (INR n)).
Replace R1 with (INR (S O)); Auto with real.
Qed.
Hints Resolve Rlt_INR1 :real.

Theorem NEq_INR: (n, m:nat) ~ n=m ->~ (INR n)==(INR m).
Intros n m H'; (Case (le_or_lt n m); Intros H'1).
Case (le_lt_or_eq ? ? H'1); Intros H'2.
Apply imp_not_Req; Auto with real.
Contradict H'; Auto.
Apply sym_not_eqT; Apply imp_not_Req; Auto with real.
Qed.
Hints Resolve NEq_INR :real.

Theorem NEq_INRO: (n:nat) ~ n=O ->~ (INR n)==R0.
Replace R0 with (INR O); Auto with real.
Qed.
Hints Resolve NEq_INRO :real.

Theorem NEq_INR1: (n:nat) ~ n=(S O) ->~ (INR n)==R1.
Replace R1 with (INR (S O)); Auto with real.
Qed.
Hints Resolve NEq_INR1 :real.

Theorem not_O_lt: (n:nat) ~ n=O ->(lt O n).
Intros n; Elim n; Simpl; Auto with arith.
Qed.
Hints Resolve not_O_lt :arith.

Theorem Rlt_IZR: (p, q:Z) (Zlt p q) ->(Rlt (IZR p) (IZR q)).
Intros p q H'; Apply Rminus_lt.
Rewrite <- Rminus_IZR.
Cut (Zlt (Zminus p q) ZERO).
Case (Zminus p q); Simpl; Auto.
Intros H'0; Contradict H'0; Auto.
Apply Zlt_n_n; Auto.
Simpl.
Intros p0 H'0; Contradict H'0; Auto.
Apply Zlt_not_sym; Unfold Zlt; Simpl; Auto.
Intros p0 H'0; Apply Rgt_RoppO.
Red; Auto with real arith.
Apply Zsimpl_lt_plus_l with p := q; Auto with zarith.
Rewrite Zle_plus_minus; Auto with zarith.
Rewrite <- Zplus_n_O; Auto.
Qed.
Hints Resolve Rlt_IZR :real.

Theorem Rle_IZR: (x, y:Z) (Zle x y) ->(Rle (IZR x) (IZR y)).
Intros x y H'.
Case (Zle_lt_or_eq ? ? H'); Clear H'; Intros H'.
Apply Rlt_le; Auto with real.
Rewrite <- H'; Auto with real.
Qed.
Hints Resolve Rle_IZR :real.

Theorem lt_Rlt: (n, m:nat) (Rlt (INR n) (INR m)) ->(lt n m).
Intros n m H'; Case (le_or_lt m n); Auto; Intros H0; Contradict H';
Auto with real.
Case (le_lt_or_eq ? ? H0); Intros H1; Auto with real.
Rewrite H1; Apply Rlt_antirefl.
Qed.

Theorem INR_inv: (n, m:nat) (INR n)==(INR m) ->n=m.
Intros n; Elim n; Auto; Try Rewrite S_INR.
Intros m; Case m; Auto.
Intros m' H1; Contradict H1; Auto.
Rewrite S_INR.
Apply imp_not_Req; Left.
Apply Rlt_r_plus_R1.
Apply INR_le.
Intros n' H' m; Case m.
Intros H'0; Contradict H'0; Auto.
Rewrite S_INR.
Apply imp_not_Req; Right.
Red; Apply Rlt_r_plus_R1.
Apply INR_le.
Intros m' H'0.
Rewrite (H' m'); Auto.
Repeat Rewrite S_INR in H'0.
Apply r_Rplus_plus with r := R1; Repeat Rewrite (Rplus_sym R1); Auto with real.
Qed.

Theorem Rle_INR: (x, y:nat) (le x y) ->(Rle (INR x) (INR y)).
Intros x y H; Repeat Rewrite INR_IZR_INZ.
Apply Rle_IZR; Auto with zarith.
Qed.
Hints Resolve Rle_INR :real.

Theorem Rmult_INR: (n, m:nat)(INR (mult n m))==(Rmult (INR n) (INR m)).
Intros n; Elim n; Auto with real.
Intros n1 H' m.
Replace (mult (S n1) m) with (plus m (mult n1 m)).
Rewrite plus_INR; Rewrite H'.
Rewrite S_INR; Simpl.
Rewrite (Rmult_sym (Rplus (INR n1) R1)); Rewrite Rmult_Rplus_distr;
Auto with real.
Rewrite (Rmult_sym (INR n1)); Rewrite Rmult_ne_l; Auto with real.
Apply Rplus_sym.
Simpl; Auto.
Qed.
Hints Resolve Rmult_INR :real.

Theorem Rmult_IZR: (z, t:Z)(IZR (Zmult z t))==(Rmult (IZR z) (IZR t)).
Intros z t; Case z; Case t; Simpl; Auto with real.
Intros t1 z1; Rewrite times_convert; Auto with real.
Intros t1 z1; Rewrite times_convert; Auto with real.
Rewrite Rmult_sym.
Rewrite Ropp_mul1; Auto with real.
Apply eq_Ropp; Rewrite mult_sym; Auto with real.
Intros t1 z1; Rewrite times_convert; Auto with real.
Rewrite Ropp_mul1; Auto with real.
Intros t1 z1; Rewrite times_convert; Auto with real.
Rewrite Ropp_mul2; Auto with real.
Qed.

Theorem absolu_Zs: (z:Z) (Zle ZERO z) ->(absolu (Zs z))=(S (absolu z)).
Intros z; Case z.
3:Intros p H'; Contradict H'; Auto with zarith.
Replace (Zs ZERO) with (inject_nat (1)).
Intros H'; Rewrite absolu_INR; Simpl; Auto.
Simpl; Auto.
Intros p H'; Rewrite <- add_un_Zs; Simpl; Auto with zarith.
Unfold convert; Rewrite convert_add_un; Auto.
Qed.
Hints Resolve Zlt_le_S :zarith.

Theorem Zlt_next: (n, m:Z) (Zlt n m) ->m=(Zs n) \/ (Zlt (Zs n) m).
Intros n m H'; Case (Zle_lt_or_eq (Zs n) m); Auto with zarith.
Qed.

Theorem Zle_next: (n, m:Z) (Zle n m) ->m=n \/ (Zle (Zs n) m).
Intros n m H'; Case (Zle_lt_or_eq ? ? H'); Auto with zarith.
Qed.

Theorem Zlt_Zopp_Inv: (p, q:Z) (Zlt (Zopp p) (Zopp q)) ->(Zlt q p).
Intros x y H'; Case (Zle_or_lt x y); Auto with zarith.
Intros H'0; Contradict H'; Auto with zarith.
Qed.

Theorem Zle_Zopp_Inv: (p, q:Z) (Zle (Zopp p) (Zopp q)) ->(Zle q p).
Intros p q H'; Case (Zle_lt_or_eq ? ? H'); Auto with zarith.
Intros H'0; Apply Zlt_le_weak; Apply Zlt_Zopp_Inv; Auto with zarith.
Intros H'1; Replace q with p; Auto with zarith.
Rewrite <- (Zopp_Zopp p); Rewrite <- (Zopp_Zopp q); Rewrite H'1; Auto.
Qed.

Theorem absolu_Zs_neg:
  (z:Z) (Zlt z ZERO) -><nat> (S (absolu (Zs z)))=(absolu z).
Intros z H'; Apply inject_nat_eq.
Rewrite inj_S.
Repeat Rewrite <- (absolu_Zopp (Zs z)).
Repeat Rewrite <- (absolu_Zopp z).
Repeat Rewrite inj_abs; Replace ZERO with (Zopp ZERO); Auto with zarith.
Unfold Zs; Ring.
Qed.

Theorem Zlt_absolu: (x:Z) (n:nat) (lt (absolu x) n) ->(Zlt x (inject_nat n)).
Intros x n; Case x; Simpl; Auto with zarith.
Replace ZERO with (inject_nat O); Auto with zarith.
Intros p; Rewrite <- (inject_nat_convert (POS p) p); Auto with zarith.
Case n; Simpl; Intros; Red; Simpl; Auto.
Qed.

Theorem inj_pred: (n:nat) ~ n=O ->(inject_nat (pred n))=(Zpred (inject_nat n)).
Intros n; Case n; Auto.
Intros H'; Contradict H'; Auto.
Intros n0 H'; Rewrite inj_S; Rewrite <- Zpred_Sn; Auto.
Qed.

Theorem Zle_abs: (p:Z)(Zle p (inject_nat (absolu p))).
Intros p; Case p; Simpl; Auto with zarith; Intros q;
Rewrite inject_nat_convert with p := (POS q); Auto with zarith.
Unfold Zle; Red; Intros H'2; Discriminate.
Qed.
Hints Resolve Zle_abs :zarith.

Theorem ZleAbs:
  (z:Z) (n:nat) (Zle (Zopp (inject_nat n)) z) -> (Zle z (inject_nat n)) ->
  (le (absolu z) n).
Intros z n H' H'0; Case (le_or_lt (absolu z) n); Auto; Intros lt.
Case (Zle_or_lt ZERO z); Intros Zle0.
Contradict H'0.
Apply Zlt_not_le; Auto.
Rewrite <- (inj_abs z); Auto with zarith.
Contradict H'.
Apply Zlt_not_le; Auto.
Replace z with (Zopp (inject_nat (absolu z))).
Apply Zlt_Zopp; Auto with zarith.
Rewrite <- absolu_Zopp.
Rewrite inj_abs; Auto with zarith.
Ring.
Replace ZERO with (Zopp ZERO); Auto with zarith.
Qed.

Theorem lt_Zlt_inv: (n, m:nat) (Zlt (INZ n) (INZ m)) ->(lt n m).
Intros n m H'; Case (le_or_lt n m); Auto.
Intros H'0.
Case (le_lt_or_eq ? ? H'0); Auto with zarith; Intros H'1.
Contradict H'.
Apply Zle_not_lt; Auto with zarith.
Rewrite H'1; Auto with zarith.
Intros H'0; Try Assumption.
Contradict H'.
Apply Zle_not_lt; Auto with zarith.
Qed.

Theorem NconvertO: (p:positive)~ (convert p)=O.
Intros p; Elim p; Unfold convert; Simpl.
Intros p0 H'; Red; Intros H'0; Discriminate.
Intros p0; Rewrite ZL6; Unfold convert.
Case (positive_to_nat p0 (1)); Simpl; Auto.
Red; Intros H'; Discriminate.
Qed.
Hints Resolve NconvertO :zarith.

Theorem absolu_lt_nz: (z:Z) ~ z=ZERO ->(lt O (absolu z)).
Intros z; Case z; Simpl; Auto; Try (Intros H'; Case H'; Auto; Fail); Intros p;
Generalize (NconvertO p); Auto with arith.
Qed.

Theorem Rlt2: (Rlt R0 (INR (S (S O)))).
Replace R0 with (INR O); Auto with real arith.
Qed.
Hints Resolve Rlt2 :real.

Theorem RlIt2: (Rlt R0 (Rinv (INR (S (S O))))).
Apply Rlt_mult_anticompatibility with z := (INR (S (S O))); Auto with real.
Rewrite Rinv_r; Auto with real.
Rewrite Rmult_Or; Auto with real.
Qed.
Hints Resolve RlIt2 :real.

Theorem Rledouble: (r:R) (Rle R0 r) ->(Rle r (Rmult (INR (S (S O))) r)).
Intros r H'.
Replace (Rmult (INR (S (S O))) r) with (Rplus r r); [Idtac | Simpl; Ring].
Pattern 1 r; Replace r with (Rplus r R0); [Idtac | Ring].
Apply Rle_compatibility; Auto.
Qed.
Hints Resolve Rledouble :real.
(*A simple database for simplification of reals *)
HintRewrite
Rsimpl
[Rplus_ne_l LR Rplus_ne_r LR Rmult_ne_l LR Rmult_ne_r LR Rplus_Ropp_r LR
Rplus_Ropp_l LR Rinv_l LR Rinv_r LR Rinv_Rmult LR Rinv_Rinv LR R1_Rinv LR
Rabsolu_Rinv LR Rmult_Or LR Rmult_Ol LR Ropp_Ropp LR Ropp_O LR Ropp_mul1 LR
Ropp_mul2 LR plus_INR LR minus_INR LR INR_IZR_INZ RL plus_IZR LR
Ropp_Ropp_IZR LR Z_R_minus LR Rabsolu_R0 LR Rabsolu_mult LR Rplus_Rminus LR
Rabsolu_R1 LR Rminus_IZR LR Rmult_INR LR Rmult_IZR LR].

14/12/100, 02:32