Rbar_compl.v

(**
This file is part of the Elfic library

Copyright (C) Aubry, Boldo, Clément, Faissole, Leclerc, Martin, Mayero

This library 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 3 of the License, or (at your option) any later version.

This library 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
COPYING file for more details.
*)

From Coq Require Import Classical_Pred_Type.
From Coq Require Import FunctionalExtensionality.
From Coq Require Import Reals Lra List.
From Coquelicot Require Import Coquelicot.

Require Import R_compl.


Lemma Rbar_eq_le : forall x y : Rbar, x = y -> Rbar_le x y.
Proof.
intros x y H; rewrite H; apply Rbar_le_refl.
Qed.

Ltac trans0 :=
  try match goal with
  (* validation du but par transitivite de l'egalite *)
  | H1 : (?X1 = ?X2),
    H2 : (?X2 = ?X3) |- (?X1 = ?X3)
    => now apply eq_trans with (y := X2)
  | H1 : (?X1 = ?X2),
    H2 : (?X2 = ?X3) |- (?X3 = ?X1)
    => apply eq_sym;now apply eq_trans with (y := X2)
  | H1 : (?X1 = ?X2),
    H2 : (?X3 = ?X2) |- (?X1 = ?X3)
    => rewrite H1 ; now apply eq_sym
  | H1 : (?X1 = ?X2),
    H2 : (?X3 = ?X2) |- (?X3 = ?X1)
    => rewrite H1 ; now apply eq_sym

  (* transformation du but par transitivite de l'egalite *)
  | H : (?X1 = ?X2) |- (?X1 = _)
    => rewrite H
  | H : (?X1 = ?X2) |- (_ = ?X1)
    => rewrite H
  | H : (?X2 = ?X1) |- (?X1 = _)
    => rewrite <-H
  | H : (?X2 = ?X1) |- (_ = ?X1)
    => rewrite <-H

  (* =  et <> implique <> *)
  | H1 : (?X1 = ?X2),
    H2 : (?X2 <> ?X3) |- (?X1 <> ?X3)
    => now rewrite H1
  | H1 : (?X1 = ?X2),
    H2 : (?X2 <> ?X3) |- (?X3 <> ?X1)
    => apply not_eq_sym;now rewrite H1
  | H1 : (?X1 = ?X2),
    H2 : (?X3 <> ?X2) |- (?X1 <> ?X3)
    => rewrite H1 ; now apply not_eq_sym
  | H1 : (?X1 = ?X2),
    H2 : (?X3 <> ?X2) |- (?X3 <> ?X1)
    => now rewrite H1
  | H1 : (?X2 = ?X1),
    H2 : (?X3 <> ?X2) |- (?X1 <> ?X3)
    => apply not_eq_sym;now rewrite <-H1
  | H1 : (?X2 = ?X1),
    H2 : (?X3 <> ?X2) |- (?X3 <> ?X1)
    => now rewrite <-H1
  | H1 : (?X2 = ?X1),
    H2 : (?X2 <> ?X3) |- (?X1 <> ?X3)
    => now rewrite <-H1
  | H1 : (?X2 = ?X1),
    H2 : (?X2 <> ?X3) |- (?X3 <> ?X1)
    => apply not_eq_sym;now rewrite <-H1

  (* =  implique <= *)
  | H1 : (?X1 = ?X2) |- (Rbar_le ?X1 ?X2)
    => now apply Rbar_eq_le
  | H1 : (?X1 = ?X2) |- (Rbar_le ?X2 ?X1)
    => now apply Rbar_eq_le
  | H1 : (?X1 = ?X2)%R |- (Rle ?X1 ?X2)
    => now apply Req_le
  | H1 : (?X1 = ?X2)%R |- (Rle ?X2 ?X1)
    => now apply Req_le

  (* a<b  implique a<=b *)
  | H1 : Rbar_lt ?X1 ?X2 |- Rbar_le ?X1 ?X2
    => apply Rbar_lt_le
  | H1 : Rlt ?X1 ?X2 |- Rle ?X1 ?X2
    => apply Rlt_le

  (* a <= b <= c implique a <= c*)
  | H1 : Rbar_le ?X1 ?X2,
    H2 : Rbar_le ?X2 ?X3 |- Rbar_le ?X1 ?X3
    => try now apply Rbar_le_trans with X2
  | H1 : Rle ?X1 ?X2,
    H2 : Rle ?X2 ?X3 |- Rle ?X1 ?X3
    => try now apply Rle_trans with X2

  (* dans Rbar puis dans R, a < b <= c ; a < b < c et a <= b < c impliquent a < c *)
  | H1 : Rbar_lt ?X1 ?X2,
    H2 : Rbar_le ?X2 ?X3 |- Rbar_lt ?X1 ?X3
    => try now apply Rbar_lt_le_trans with X2
  | H1 : Rbar_lt ?X1 ?X2,
    H2 : Rbar_lt ?X2 ?X3 |- Rbar_lt ?X1 ?X3
    => try now apply Rbar_lt_trans with X2
  | H1 : Rbar_le ?X1 ?X2,
    H2 : Rbar_lt ?X2 ?X3 |- Rbar_lt ?X1 ?X3
    => try now apply Rbar_le_lt_trans with X2
  | H1 : Rlt ?X1 ?X2,
    H2 : Rle ?X2 ?X3 |- Rlt ?X1 ?X3
    => try now apply Rlt_le_trans with X2
  | H1 : Rlt ?X1 ?X2,
    H2 : Rlt ?X2 ?X3 |- Rlt ?X1 ?X3
    => try now apply Rlt_trans with X2
  | H1 : Rle ?X1 ?X2,
    H2 : Rlt ?X2 ?X3 |- Rlt ?X1 ?X3
    => try now apply Rle_lt_trans with X2

  (* TRANSFORMATIONS : on veut prouver x<y en s'aidant de H:x<=z
    il restera donc a charge de prouver z<y *)
  |H:Rle ?X1 ?X2 |- Rlt ?X1 ?X3 =>
     apply Rle_lt_trans with (r2:=X2)
  |H:Rbar_le ?X1 ?X2 |- Rbar_lt ?X1 ?X3 =>
     apply Rbar_le_lt_trans with (y:=X2)

  (* TRANSFORMATIONS : on veut prouver x<y en s'aidant de H:x<z
    il restera donc a charge de prouver z<y *)
  |H:Rlt ?X1 ?X2 |- Rlt ?X1 ?X3 =>
     apply Rlt_trans with (r2:=X2)
  |H:Rbar_lt ?X1 ?X2 |- Rbar_lt ?X1 ?X3 =>
     apply Rbar_lt_trans with (y:=X2)

  (* TRANSFORMATIONS : on veut prouver x<y en s'aidant de H:z<y
    il restera donc a charge de prouver z<y *)
  |H:Rlt ?X2 ?X3 |- Rlt ?X1 ?X3 =>
     apply Rlt_trans with (r2:=X2)
  |H:Rbar_lt ?X2 ?X3 |- Rbar_lt ?X1 ?X3 =>
     apply Rbar_lt_trans with (y:=X2)
  end;
  try easy.

Ltac trans1 param :=
  try match goal with
  (* TRANSFORMATIONS : on veut prouver x<y en s'aidant de x<z<y en donnant l'hypothese *)
  | param: Rlt ?X1 ?X2 |- Rlt ?X1 _
     => try apply Rlt_trans with X2
  | param: Rbar_lt ?X1 ?X2 |- Rbar_lt ?X1 _
     => try apply Rbar_lt_trans with X2

  (* TRANSFORMATIONS : on veut prouver x<y en s'aidant de x<z<y en donnant z*)
  | |- Rlt _ _ =>
     try apply Rlt_trans with param ;
     try apply Rlt_trans with (2:=param)
  | |- Rbar_lt _ _ =>
     try apply Rbar_lt_trans with param ;
     try apply Rbar_lt_trans with (2:=param)

  (* TRANSFORMATIONS : on veut prouver x<=y en s'aidant de x<=z et de z<=y en donnant l'hypothese *)
  | param: Rle ?X1 ?X2 |- Rle ?X1 _
     => try apply Rle_trans with X2
  | param: Rbar_le ?X1 ?X2 |- Rbar_le ?X1 _
     => try apply Rbar_le_trans with X2

  (* TRANSFORMATIONS : on veut prouver x<=y en s'aidant de x<=z et de z<=y en donnant z *)
  | |- Rle _ _ =>
     try apply Rle_trans with param ;
     try apply Rle_trans with (2:=param)
    (*  ;try apply Rlt_le *)
  | |- Rbar_le _ _ =>
     try apply Rbar_le_trans with param ;
     try apply Rbar_le_trans with (2:=param)

  (* transitivite de l'egalite *)
  | param : (?X1 = ?X2) |- (?X1 = _)
    => now rewrite param

  | param : (?X2 = ?X1) |- (?X1 = _)
    => now rewrite <-param

  (* =  et <> implique <> *)
  | param : (?X1 = ?X2),
    H2 : (?X2 <> ?X3) |- (?X1 <> ?X3)
    => first [now rewrite param|apply not_eq_sym;now rewrite param]

  | param : (?X1 = ?X2),
    H2 : (?X3 <> ?X2) |- (?X1 <> ?X3)
    => first [now rewrite param|apply not_eq_sym;now rewrite param]

  | param : (?X2 = ?X1),
    H2 : (?X3 <> ?X2) |- (?X1 <> ?X3)
    => first [now rewrite <-param|apply not_eq_sym;now rewrite <-param]

  | param : (?X2 = ?X1),
    H2 : (?X2 <> ?X3) |- (?X1 <> ?X3)
    => first [now rewrite <-param|apply not_eq_sym;now rewrite <-param]

  (* =  implique <= *)
  | param : (?X1 = ?X2) |- (Rbar_le ?X1 ?X2)
    => now apply Rbar_eq_le
  | param : (?X1 = ?X2) |- (Rbar_le ?X2 ?X1)
    => now apply Rbar_eq_le
  | param : (?X1 = ?X2)%R |- (Rle ?X1 ?X2)
    => now apply Req_le
  | param : (?X1 = ?X2)%R |- (Rle ?X2 ?X1)
    => now apply Req_le

  (* a <= b <= c implique a <= c*)
  | H1 : Rbar_le ?X1 ?X2,
    H2 : Rbar_le ?X2 ?X3 |- Rbar_le ?X1 ?X3
    => first [now apply Rbar_le_trans with param | now apply Rbar_le_trans with (2:=param)]
  | H1 : Rle ?X1 ?X2,
    H2 : Rle ?X2 ?X3 |- Rle ?X1 ?X3
    => first [now apply Rle_trans with (param) | now apply Rle_trans with (2:=param)]

  (* dans Rbar puis dans R, a < b <= c ; a < b < c et a <= b < c impliquent a < c *)
  | H1 : Rbar_lt ?X1 ?X2,
    H2 : Rbar_le ?X2 ?X3 |- Rbar_lt ?X1 ?X3
    => first [now apply Rbar_lt_le_trans with (param) | now apply Rbar_lt_le_trans with (2:=param)]
  | H1 : Rbar_lt ?X1 ?X2,
    H2 : Rbar_lt ?X2 ?X3 |- Rbar_lt ?X1 ?X3
    => first [now apply Rbar_lt_trans with (param) | now apply Rbar_lt_trans with (2:=param)]
  | H1 : Rbar_le ?X1 ?X2,
    H2 : Rbar_lt ?X2 ?X3 |- Rbar_lt ?X1 ?X3
    => first [now apply Rbar_le_lt_trans with (param) | now apply Rbar_le_lt_trans with (2:=param)]
  | H1 : Rlt ?X1 ?X2,
    H2 : Rle ?X2 ?X3 |- Rlt ?X1 ?X3
    => first [now apply Rlt_le_trans with (param) | now apply Rlt_le_trans with (2:=param)]
  | H1 : Rlt ?X1 ?X2,
    H2 : Rlt ?X2 ?X3 |- Rlt ?X1 ?X3
    => first [now apply Rlt_trans with (param) | now apply Rlt_trans with (2:=param)]
  | H1 : Rle ?X1 ?X2,
    H2 : Rlt ?X2 ?X3 |- Rlt ?X1 ?X3
    => first [now apply Rle_lt_trans with (param) | now apply Rle_lt_trans with (2:=param)]
  end;
  try easy.

(*
Appel de la tactique trans avec 2 parametres,
le 2e indiquant la ou doit etre mis le "leq" (inferieur ou egal) comme suit :
- 0 ou autre indique aucun des 2 cotes
- 1 indique le leq a gauche (1re inegalite)
- 2 insique leq a droite (2e inegalite)
- 3 ou plus : a gauche ET a droite (dans les 2 inegalites)
*)
Ltac trans2 param placeLeq :=
  match goal with
  (* TRANSFORMATIONS (sur R puis sur Rbar) : on veut prouver a<b en s'aidant de
	a<=c<b
	a<c<=b
	a<c<b
  *)
  | |- Rlt _ _ =>
    match placeLeq with
    | 1 =>
      try apply Rle_lt_trans with param ;
      try apply Rle_lt_trans with (2:=param)
    | 2 =>
      try apply Rlt_le_trans with param ;
      try apply Rlt_le_trans with (2:=param)
    | _ =>
      try apply Rlt_trans with param ;
      try apply Rlt_trans with (2:=param)
    end
  | |- Rbar_lt _ _ =>
    match placeLeq with
    | 1 =>
      try apply Rbar_le_lt_trans with param ;
      try apply Rbar_le_lt_trans with (2:=param)
    | 2 =>
      try apply Rbar_lt_le_trans with param ;
      try apply Rbar_lt_le_trans with (2:=param)
    | _ =>
      try apply Rbar_lt_trans with param ;
      try apply Rbar_lt_trans with (2:=param)
    end

  (* TRANSFORMATIONS (sur R puis sur Rbar) : on veut prouver a<=b en s'aidant de
  a<b<c   avec placeLeq = 0
	a<=c<b  avec placeLeq = 1
	a<c<=b  avec placeLeq = 2
	a<=c<=b avec placeLeq >= 3
  *)
  | |- Rle _ _ =>
    match placeLeq with
    | 0 =>
      apply Rlt_le;
      try apply Rlt_trans with param ;
      try apply Rlt_trans with (2:=param)
    | 1 =>
      try apply Rle_lt_trans with param ;
      try apply Rle_lt_trans with (2:=param)
    | 2 =>
      apply Rle_trans with param
    | _ =>
      try apply Rle_trans with param ;
      try apply Rle_trans with (2:=param)
    end
  | |- Rbar_le _ _ =>
    match placeLeq with
    | 0 =>
      apply Rbar_lt_le;
      try apply Rbar_lt_trans with param ;
      try apply Rbar_lt_trans with (2:=param)
    | 1 =>
      try apply Rbar_le_lt_trans with param ;
      try apply Rbar_le_lt_trans with (2:=param)
    | 2 =>
      apply Rbar_le_trans with param ; apply Rbar_lt_le
    | _ =>
      try apply Rbar_le_trans with param ;
      try apply Rbar_le_trans with (2:=param)
    end
  end;
  try easy.

Tactic Notation "trans" :=
  trans0.
Tactic Notation "trans" constr(x) :=
  trans1 x.
Tactic Notation "trans" constr(x) constr(y) :=
  trans2 x y.
Tactic Notation "trans" constr(x) "with" "(leq:=" constr(y) ")" :=
  trans2 x y.


Section Rbar_atan_compl.

(** Atan Lipschitz on Rbar. *)

Definition Rbar_atan : Rbar -> R :=
  fun x => match x with
    | p_infty => PI/2
    | Finite r => atan r
    | m_infty => -PI/2
    end.

Lemma Rbar_atan_Lipschitz :
  forall x y,
    Rbar_le
      (Rbar_abs (Rbar_minus (Rbar_atan x) (Rbar_atan y)))
      (Rbar_abs (Rbar_minus x y)).
Proof.
intros x y.
case x; case y; simpl; try easy; try (f_equal; apply Req_le).
intros; apply atan_Lipschitz.
replace (PI / 2 + - (PI / 2)) with 0; auto with real.
replace (- PI / 2 + - (- PI / 2)) with 0; auto with real.
Qed.

Lemma Rbar_atan_increasing :
  forall x y, Rbar_lt x y -> Rbar_atan x < Rbar_atan y.
Proof.
intros x y; case x; case y; try easy.
simpl; intros a b H.
now apply atan_increasing.
simpl; intros a _.
apply atan_bound.
simpl; intros a _.
apply atan_bound.
simpl; intros _.
trans (atan 0); apply atan_bound.
Qed.

Lemma Rbar_atan_increasing_rev :
  forall x y, Rbar_atan x < Rbar_atan y -> Rbar_lt x y.
Proof.
intros x y H.
case (Rbar_lt_le_dec x y); try easy.
intros H1.
contradict H; apply Rle_not_lt.
case (Rbar_le_lt_or_eq_dec _ _ H1).
intros H2; left; apply Rbar_atan_increasing; easy.
intros H3; rewrite H3;now right.
Qed.

Lemma Rbar_atan_increasing_equiv :
  forall x y, Rbar_lt x y <-> Rbar_atan x < Rbar_atan y.
Proof.
intros; split.
apply Rbar_atan_increasing.
apply Rbar_atan_increasing_rev.
Qed.

End Rbar_atan_compl.


Section Rbar_R_compat_compl.

(** Complements on compatibility with real numbers. *)

(* Lemmas Rbar_finite_eq and Rbar_finite_neq are already in Coquelicot. *)

Lemma Rbar_eq_real :
  forall x y : Rbar,
    is_finite x -> is_finite y ->
    x = y <-> real x = real y.
Proof.
intros x y Hx Hy.
apply is_finite_correct in Hx; destruct Hx as [a Ha].
apply is_finite_correct in Hy; destruct Hy as [b Hb].
rewrite Ha, Hb; simpl.
split; apply Rbar_finite_eq.
Qed.

Lemma Rbar_neq_real :
  forall x y : Rbar,
    is_finite x -> is_finite y ->
    x <> y <-> real x <> real y.
Proof.
intros x y Hx Hy.
apply is_finite_correct in Hx; destruct Hx as [a Ha].
apply is_finite_correct in Hy; destruct Hy as [b Hb].
rewrite Ha, Hb; simpl.
split; apply Rbar_finite_neq.
Qed.

(* Useful? *)
Lemma Rbar_finite_le : forall x y : R, Rbar_le (Finite x) (Finite y) <-> x <= y.
Proof.
intros x y; now simpl.
Qed.

Lemma Rbar_le_real :
  forall x y : Rbar,
    is_finite x -> is_finite y ->
    Rbar_le x y <-> real x <= real y.
Proof.
intros x y Hx Hy.
apply is_finite_correct in Hx; destruct Hx as [a Ha].
apply is_finite_correct in Hy; destruct Hy as [b Hb].
rewrite Ha, Hb; now simpl.
Qed.

(* Useful? *)
Lemma Rbar_finite_opp : forall x : R, Rbar_opp (Finite x) = Finite (- x).
Proof.
intros x; now simpl.
Qed.

(* Lemma Rbar_opp_real is already in Coquelicot. *)

(* Useful? *)
Lemma Rbar_finite_plus :
  forall x y : R, Rbar_plus (Finite x) (Finite y) = Finite (x + y).
Proof.
intros x y; now simpl.
Qed.

Lemma Rbar_plus_real :
  forall x y : Rbar,
    is_finite x -> is_finite y ->
    real (Rbar_plus x y) = real x + real y.
Proof.
intros x y Hx Hy.
apply is_finite_correct in Hx; destruct Hx as [a Ha].
apply is_finite_correct in Hy; destruct Hy as [b Hb].
rewrite Ha, Hb; now simpl.
Qed.

(* Useful? *)
Lemma Rbar_finite_minus :
  forall x y : R, Rbar_minus (Finite x) (Finite y) = Finite (x - y).
Proof.
intros x y; now simpl.
Qed.

Lemma Rbar_minus_real :
  forall x y : Rbar,
    is_finite x -> is_finite y ->
    real (Rbar_minus x y) = real x - real y.
Proof.
intros x y Hx Hy.
apply is_finite_correct in Hx; destruct Hx as [a Ha].
apply is_finite_correct in Hy; destruct Hy as [b Hb].
rewrite Ha, Hb; now simpl.
Qed.

(* Useful? *)
Lemma Rbar_finite_mult :
  forall x y : R, Rbar_mult (Finite x) (Finite y) = Finite (x * y).
Proof.
intros x y; now simpl.
Qed.

Lemma Rbar_mult_real :
  forall x y : Rbar,
    is_finite x -> is_finite y ->
    real (Rbar_mult x y) = real x * real y.
Proof.
intros x y Hx Hy.
apply is_finite_correct in Hx; destruct Hx as [a Ha].
apply is_finite_correct in Hy; destruct Hy as [b Hb].
rewrite Ha, Hb; now simpl.
Qed.

(* Useful? *)
Lemma Rbar_finite_div :
  forall x y : R, Rbar_div (Finite x) (Finite y) = Finite (x / y).
Proof.
intros x y; now simpl.
Qed.

Lemma Rbar_div_real :
  forall x y : Rbar,
    is_finite x -> is_finite y ->
    real (Rbar_div x y) = real x / real y.
Proof.
intros x y Hx Hy.
apply is_finite_correct in Hx; destruct Hx as [a Ha].
apply is_finite_correct in Hy; destruct Hy as [b Hb].
rewrite Ha, Hb; now simpl.
Qed.

Lemma In_map_Finite : forall x l, In x (map Finite l) -> In (real x) l.
Proof.
intros x l; case x.
intros r; simpl.
rewrite in_map_iff.
intros (y,(Hy1,Hy2)).
injection Hy1; intros T; now rewrite <- T.
intros T.
rewrite in_map_iff in T.
destruct T as (y,(Hy1,Hy2)); easy.
intros T.
rewrite in_map_iff in T.
destruct T as (y,(Hy1,Hy2)); easy.
Qed.

End Rbar_R_compat_compl.


Section Rbar_order_compl.

(** Complements on Rbar_le/Rbar_lt. *)

Lemma Rbar_abs_ge_0 : forall x, Rbar_le 0 (Rbar_abs x).
Proof.
intros x; case x; try easy.
intros r; apply Rabs_pos.
Qed.

Lemma Rbar_abs_le_between : forall x y : Rbar,
       Rbar_le (Rbar_abs x) y <->
       Rbar_le (Rbar_opp y) x /\ Rbar_le x y.
Proof.
intros x y; case x; case y; try easy.
intros u v; simpl; apply Rabs_le_between.
Qed.

Lemma Rbar_abs_triang : forall x y: Rbar,
  Rbar_le (Rbar_abs (Rbar_plus x y)) (Rbar_plus (Rbar_abs x) (Rbar_abs y)).
Proof.
intros x y; case x; case y; try easy.
intros r1 r2; simpl.
apply Rabs_triang.
Qed.

Lemma Rbar_minus_le_0: forall a b : Rbar, Rbar_le a b -> Rbar_le 0 (Rbar_minus b a).
Proof.
intros a b; case a; case b; simpl; try easy.
intros x y; apply Rminus_le_0.
intros _; apply Rle_refl.
intros _; apply Rle_refl.
Qed.

Lemma Rbar_le_eq : forall x y z, x = y -> Rbar_le y z -> Rbar_le x z.
Proof.
intros x y z H1 H2.
trans H2; trans.
Qed.

Lemma Rbar_le_cases :
  forall x, Rbar_le 0 x ->
    x = Finite 0 \/
    (exists r:R, 0 < r /\ x = Finite r) \/
    x = p_infty.
Proof.
intro x.
case x ; simpl.
intros y H.
destruct H.
right.
left.
exists y.
tauto.
left.
apply eq_sym.
rewrite <- H.
trivial.
right ; right ; trivial.
apply except.
Qed.

Lemma Rbar_bounded_is_finite :
  forall x y z,
    Rbar_le x y -> Rbar_le y z ->
    is_finite x -> is_finite z -> is_finite y.
Proof.
intros x y z; case x; case y; case z; now intros.
Qed.

Lemma Rbar_le_finite_eq_rle :
  forall x y,
    is_finite x -> is_finite y ->
    Rbar_le x y = Rle (real x) (real y).
Proof.
intros x y Hx Hy.
destruct x, y ; easy.
Qed.

Lemma Rbar_lt_finite_eq_rlt :
  forall x y,
    is_finite x -> is_finite y ->
    Rbar_lt x y = Rlt (real x) (real y).
Proof.
intros x y Hx Hy.
destruct x, y ; easy.
Qed.

Lemma not_Rbar_le_finite_minfty :
  forall x, is_finite x -> Rbar_le x m_infty -> False.
Proof.
intros x H1 H2.
rewrite <- H1 in H2.
easy.
Qed.

Lemma not_Rbar_ge_finite_pinfty :
  forall x, is_finite x -> Rbar_le p_infty x -> False.
Proof.
intros x Hx Hy.
rewrite <-Hx in Hy.
easy.
Qed.

Lemma Rbar_le_finite_pinfty :
  forall x, is_finite x -> Rbar_le x p_infty.
Proof.
intros x Hx.
case x ; try intros ; easy.
Qed.

Lemma Rbar_le_minfty_finite :
  forall x, is_finite x -> Rbar_le m_infty x.
Proof.
intros x Hx.
case x ; try intros ; easy.
Qed.

Lemma Rbar_lt_increasing :
  forall u N,
    (forall i, (i < N )%nat -> Rbar_lt (u i) (u (S i))) ->
    forall i j, (i <= j <= N)%nat -> Rbar_le (u i) (u j).
Proof.
intros u N H i j Hij.
replace j with (i+(j-i))%nat by auto with zarith.
cut (j-i <= N)%nat; try auto with zarith.
cut (i+ (j-i) <= N)%nat; try auto with zarith.
generalize ((j-i))%nat.
induction n; intros M1 M2.
rewrite plus_0_r.
apply Rbar_le_refl.
trans (u (i+n)%nat).
apply IHn; auto with zarith.
replace (i+ S n)%nat with (S (i+n)) by auto with zarith.
apply Rbar_lt_le, H.
auto with zarith.
Qed.

Lemma Rbar_le_increasing :
  forall u N,
    (forall i, (i < N )%nat -> Rbar_le (u i) (u (S i))) ->
    forall i j, (i <= j <= N)%nat -> Rbar_le (u i) (u j).
Proof.
intros u N H i j Hij.
replace j with (i+(j-i))%nat by auto with zarith.
cut (j-i <= N)%nat; try auto with zarith.
cut (i+ (j-i) <= N)%nat; try auto with zarith.
generalize ((j-i))%nat.
induction n; intros M1 M2.
rewrite plus_0_r.
apply Rbar_le_refl.
trans (u (i+n)%nat).
apply IHn; auto with zarith.
replace (i+ S n)%nat with (S (i+n)) by auto with zarith.
apply H.
auto with zarith.
Qed.

Definition Rbar_max : Rbar -> Rbar -> Rbar :=
  fun x y => match x , y with
    | _ , p_infty | p_infty , _ => p_infty
    | z , m_infty | m_infty , z => z
    | Finite x , Finite y => Rmax x y
    end.

Lemma Rbar_max_comm : forall x y, Rbar_max x y = Rbar_max y x.
Proof.
intros x y; case x; case y; simpl; try easy.
intros a b; now rewrite Rmax_comm.
Qed.

Lemma Rbar_max_right : forall x y, Rbar_le x y -> Rbar_max x y = y.
Proof.
intros x y; case x; case y; try easy.
simpl; intros a b H.
now rewrite Rmax_right.
Qed.

Lemma Rbar_max_left : forall x y, Rbar_le y x -> Rbar_max x y = x.
Proof.
intros x y; case x; case y; try easy.
simpl; intros a b H.
now rewrite Rmax_left.
Qed.

Definition Rbar_min : Rbar -> Rbar -> Rbar :=
  fun x y => match x , y with
    | _ , m_infty | m_infty , _ => m_infty
    | z , p_infty | p_infty , z => z
    | Finite x , Finite y => Rmin x y
    end.

End Rbar_order_compl.


Section Rbar_plus_minus_compl.

(** Complements on Rbar_plus/Rbar_minus. *)

Lemma Rbar_plus_assoc :
  forall x y z,
    (Rbar_le 0 x) -> (Rbar_le 0 y) -> (Rbar_le 0 z) ->
    Rbar_plus (Rbar_plus  x y) z = Rbar_plus x (Rbar_plus y z).
Proof.
intros x y z.
case x; case y; case z; simpl; intros; try easy.
f_equal; ring.
Qed.

Lemma Rbar_minus_plus_r :
  forall x y, is_finite y -> x = Rbar_minus (Rbar_plus x y) y.
Proof.
intros x y; case x; case y; simpl; try easy; intros; f_equal; ring.
Qed.

Lemma Rbar_plus_minus_r :
  forall x y, is_finite y -> x = Rbar_plus (Rbar_minus x y) y.
Proof.
intros x y; case x; case y; simpl; try easy; intros; f_equal; ring.
Qed.

Lemma Rbar_plus_minus_l :
  forall x y, is_finite x -> y = Rbar_plus x (Rbar_plus (Rbar_opp x) y).
Proof.
intros x y; case x; case y; simpl; try easy; intros; f_equal; ring.
Qed.

Lemma Rbar_minus_plus_l :
  forall x y, is_finite x -> y = Rbar_plus (Rbar_opp x) (Rbar_plus x y).
Proof.
intros x y; case x; case y; simpl; try easy; intros; f_equal; ring.
Qed.

Lemma Rbar_plus_eq_compat_l :
  forall x y z, x = y -> Rbar_plus z x = Rbar_plus z y.
Proof.
intros x y z; case x; case y; case z; try easy; simpl.
intros r r2 r1 H.
apply Rbar_finite_eq in H.
now apply Rbar_finite_eq, Rplus_eq_compat_l.
Qed.

Lemma Rbar_plus_eq_compat_r :
  forall x y z, x = y -> Rbar_plus x z = Rbar_plus y z.
Proof.
intros x y z; case x; case y; case z; try easy; simpl.
intros r r2 r1 H.
apply Rbar_finite_eq in H.
now apply Rbar_finite_eq, Rplus_eq_compat_r.
Qed.

Lemma Rbar_plus_eq_reg_l :
  forall x y z, is_finite x -> Rbar_plus x y = Rbar_plus x z -> y = z.
Proof.
intros x y z.
case x; case y; case z; intros c; try easy; intros b a Ha H.
f_equal; now apply Rplus_eq_reg_l with a, Rbar_finite_eq.
Qed.

Lemma Rbar_plus_eq_reg_r :
  forall x y z, is_finite x -> Rbar_plus y x = Rbar_plus z x -> y = z.
Proof.
intros x y z.
case x; case y; case z; intros c; try easy; intros b a Ha H.
f_equal; now apply Rplus_eq_reg_r with a, Rbar_finite_eq.
Qed.

Lemma Rbar_minus_eq_reg_l :
  forall x y z, is_finite x -> Rbar_minus x y = Rbar_minus x z -> y = z.
Proof.
intros x y z.
case x; case y; case z; intros c; try easy; intros b a Ha H.
f_equal; apply Rplus_eq_reg_l with (-a).
replace (-a + b) with (-(a - b)); try ring.
replace (-a + c) with (-(a - c)); try ring.
now apply Ropp_eq_compat, Rbar_finite_eq.
Qed.

Lemma Rbar_minus_eq_reg_r :
  forall x y z, is_finite x -> Rbar_minus y x = Rbar_minus z x -> y = z.
Proof.
intros x y z.
case x; case y; case z; intros c; try easy; intros b a Ha H.
f_equal; now apply Rplus_eq_reg_r with (-a), Rbar_finite_eq.
Qed.

Lemma Rbar_plus_le_compat_l :
  forall x y z, Rbar_le x y -> Rbar_le (Rbar_plus z x) (Rbar_plus z y).
Proof.
intros x y z.
case x; case y; case z; simpl; auto with real.
Qed.

Lemma Rbar_plus_le_compat_r :
  forall x y z, Rbar_le x y -> Rbar_le (Rbar_plus x z) (Rbar_plus y z).
Proof.
intros x y z.
case x; case y; case z; simpl; auto with real.
Qed.

Lemma Rbar_plus_lt_compat_l :
  forall x y z, is_finite x -> Rbar_lt y z -> Rbar_lt (Rbar_plus x y) (Rbar_plus x z).
Proof.
intros x y z.
case x; case y; case z; intros c; try easy; simpl; intros b a Ha.
apply Rplus_lt_compat_l.
Qed.

Lemma Rbar_plus_lt_compat_r :
  forall x y z, is_finite x -> Rbar_lt y z -> Rbar_lt (Rbar_plus y x) (Rbar_plus z x).
Proof.
intros x y z.
case x; case y; case z; intros c; try easy; simpl; intros b a Ha.
apply Rplus_lt_compat_r.
Qed.

Lemma Rbar_plus_le_reg_l :
  forall x y z, is_finite x -> Rbar_le (Rbar_plus x y) (Rbar_plus x z) -> Rbar_le y z.
Proof.
intros x y z.
case x; case y; case z; intros c; try easy; simpl; intros b a Ha.
apply Rplus_le_reg_l.
Qed.

Lemma Rbar_plus_le_reg_r :
  forall x y z, is_finite x -> Rbar_le (Rbar_plus y x) (Rbar_plus z x) -> Rbar_le y z.
Proof.
intros x y z.
case x; case y; case z; intros c; try easy; simpl; intros b a Ha.
apply Rplus_le_reg_r.
Qed.

Lemma Rbar_plus_lt_reg_l :
  forall x y z, is_finite x -> Rbar_lt (Rbar_plus x y) (Rbar_plus x z) -> Rbar_lt y z.
Proof.
intros x y z.
case x; case y; case z; intros c; try easy; simpl; intros b a Ha.
apply Rplus_lt_reg_l.
Qed.

Lemma Rbar_plus_lt_reg_r :
  forall x y z, is_finite x -> Rbar_lt (Rbar_plus y x) (Rbar_plus z x) -> Rbar_lt y z.
Proof.
intros x y z.
case x; case y; case z; intros c; try easy; simpl; intros b a Ha.
apply Rplus_lt_reg_r.
Qed.

Lemma Rbar_plus_le_0 :
  forall x y, Rbar_le 0 x -> Rbar_le 0 y -> Rbar_le 0 (Rbar_plus x y).
Proof.
intros.
replace (Finite 0) with (Rbar_plus (Finite 0) (Finite 0)).
apply Rbar_plus_le_compat ; try easy.
apply Rbar_plus_0_l.
Qed.

Lemma Rbar_plus_lt_0 :
  forall x y, Rbar_lt 0 x -> Rbar_lt 0 y -> Rbar_lt 0 (Rbar_plus x y).
Proof.
intros.
replace (Finite 0) with (Rbar_plus (Finite 0) (Finite 0)).
apply Rbar_plus_lt_compat ; try easy.
apply Rbar_plus_0_l.
Qed.

Lemma Rbar_plus_lt_neg_minfty :
  forall x, Rbar_lt x 0 -> Rbar_plus x m_infty = m_infty.
Proof.
intros x; case x; simpl; easy.
Qed.

Lemma Rbar_plus_pos_pinfty :
  forall x, Rbar_le 0 x -> Rbar_plus x p_infty = p_infty.
Proof.
intros x; case x; simpl; easy.
Qed.

Lemma Rbar_plus_real_minfty :
  forall x, Rbar_lt x p_infty -> Rbar_plus x m_infty = m_infty.
Proof.
intros x; case x; now simpl.
Qed.

Lemma Rbar_plus_lt_pos_pos_pos :
  forall a b : Rbar, Rbar_lt 0 a -> Rbar_lt 0 b -> Rbar_lt 0 (Rbar_plus a b).
Proof.
intros.
destruct a.
destruct b.
apply Rplus_lt_0_compat; try easy.
rewrite Rbar_plus_pos_pinfty.
easy.
now apply Rbar_lt_le.
now rewrite Rbar_plus_real_minfty.
rewrite Rbar_plus_comm.
rewrite Rbar_plus_pos_pinfty.
easy.
now apply Rbar_lt_le.
rewrite Rbar_plus_comm.
destruct b.
now rewrite Rbar_plus_real_minfty.
exfalso.
contradict H.
exfalso.
contradict H.
Qed.

Lemma ex_Rbar_plus_ge_0 :
  forall x y, Rbar_le 0 x -> Rbar_le 0 y -> ex_Rbar_plus x y.
Proof.
intros x y; unfold ex_Rbar_plus, Rbar_plus'.
case x; case y; easy.
Qed.

End Rbar_plus_minus_compl.


Section Rbar_mult_compl.

(** Complements on Rbar_mult. *)

Lemma Rbar_mult_lt_pos_pinfty :
  forall x, (Rbar_lt 0 x) -> Rbar_mult p_infty x = p_infty.
Proof.
intros x; case x; simpl; try easy.
intros r Hr.
case (Rle_dec 0 r).
intros H1; case (Rle_lt_or_eq_dec 0 r H1); try easy.
intros K; contradict K.
now apply Rlt_not_eq.
intros K; contradict K.
now left.
Qed.

Lemma Rbar_mult_lt_pos_minfty :
  forall x, Rbar_lt 0 x -> Rbar_mult m_infty x = m_infty.
Proof.
intros x; case x; simpl; try easy.
intros r Hr.
case (Rle_dec 0 r).
intros H1; case (Rle_lt_or_eq_dec 0 r H1); try easy.
intros K; contradict K.
now apply Rlt_not_eq.
intros K; contradict K.
now left.
Qed.

Lemma Rbar_mult_lt_neg_pinfty :
  forall x, (Rbar_lt x 0) -> Rbar_mult p_infty x = m_infty.
Proof.
intros x; case x; simpl; try easy.
intros r Hr.
case (Rle_dec 0 r);auto.
intros H1; case (Rle_lt_or_eq_dec 0 r H1); try easy.
intros K; contradict K.
apply Rle_not_lt;now left.
intros K; contradict K.
red;intro;symmetry in H.
generalize H.
now apply Rlt_not_eq.
Qed.