Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(*********************************************************)
Complements for the real numbers
(*                                                       *)
(*********************************************************)

Require Import Rbase.
Require Import R_Ifp.
Local Open Scope R_scope.

Implicit Type r : R.

(*******************************)

Rmin

(*******************************)

(*********)
Definition Rmin (x y:R) : R :=
  match Rle_dec x y with
    | left _ => x
    | right _ => y
  end.

(*********)

forall (r1 r2 : R) (P : R -> Type), P r1 -> P r2 -> P (Rmin r1 r2)

forall (r1 r2 : R) (P : R -> Type), P r1 -> P r2 -> P (Rmin r1 r2)
intros r1 r2 P H1 H2; unfold Rmin; case (Rle_dec r1 r2); auto. Qed. (*********)

forall (r1 r2 : R) (P : R -> Type), (r1 <= r2 -> P r1) -> (r2 <= r1 -> P r2) -> P (Rmin r1 r2)

forall (r1 r2 : R) (P : R -> Type), (r1 <= r2 -> P r1) -> (r2 <= r1 -> P r2) -> P (Rmin r1 r2)
intros r1 r2 P H1 H2; unfold Rmin; destruct (Rle_dec r1 r2); auto with real. Qed. (*********)

forall r1 r2 r : R, Rmin r1 r2 > r -> r1 > r /\ r2 > r

forall r1 r2 r : R, Rmin r1 r2 > r -> r1 > r /\ r2 > r
r1, r2, r:R
Hle:r1 <= r2
H:r1 > r

r1 > r /\ r2 > r
r1, r2, r:R
Hnle:~ r1 <= r2
H:r2 > r
r1 > r /\ r2 > r
r1, r2, r:R
Hle:r1 <= r2
H:r1 > r

r1 > r
r1, r2, r:R
Hle:r1 <= r2
H:r1 > r
r2 > r
r1, r2, r:R
Hnle:~ r1 <= r2
H:r2 > r
r1 > r /\ r2 > r
r1, r2, r:R
Hle:r1 <= r2
H:r1 > r

r2 > r
r1, r2, r:R
Hnle:~ r1 <= r2
H:r2 > r
r1 > r /\ r2 > r
r1, r2, r:R
Hnle:~ r1 <= r2
H:r2 > r

r1 > r /\ r2 > r
r1, r2, r:R
Hnle:~ r1 <= r2
H:r2 > r

r1 > r
r1, r2, r:R
Hnle:~ r1 <= r2
H:r2 > r
r2 > r
r1, r2, r:R
Hnle:~ r1 <= r2
H:r2 > r

r2 > r
assumption. Qed. (*********)

forall r1 r2 r : R, r1 > r /\ r2 > r -> Rmin r1 r2 > r

forall r1 r2 r : R, r1 > r /\ r2 > r -> Rmin r1 r2 > r
intros; unfold Rmin; case (Rle_dec r1 r2); elim H; clear H; intros; assumption. Qed. (*********)

forall r1 r2 r : R, Rmin r1 r2 > r <-> r1 > r /\ r2 > r

forall r1 r2 r : R, Rmin r1 r2 > r <-> r1 > r /\ r2 > r
r1, r2, r:R

Rmin r1 r2 > r -> r1 > r /\ r2 > r
r1, r2, r:R
r1 > r /\ r2 > r -> Rmin r1 r2 > r
r1, r2, r:R

r1 > r /\ r2 > r -> Rmin r1 r2 > r
exact (Rmin_Rgt_r r1 r2 r). Qed. (*********)

forall x y : R, Rmin x y <= x

forall x y : R, Rmin x y <= x
intros; unfold Rmin; case (Rle_dec x y); intro H1; [ right; reflexivity | auto with real ]. Qed. (*********)

forall x y : R, Rmin x y <= y

forall x y : R, Rmin x y <= y
intros; unfold Rmin; case (Rle_dec x y); intro H1; [ assumption | auto with real ]. Qed. (*********)

forall x y : R, x <= y -> Rmin x y = x

forall x y : R, x <= y -> Rmin x y = x
intros; apply Rmin_case_strong; auto using Rle_antisym. Qed. (*********)

forall x y : R, y <= x -> Rmin x y = y

forall x y : R, y <= x -> Rmin x y = y
intros; apply Rmin_case_strong; auto using Rle_antisym. Qed. (*********)

forall x y z : R, x <= y -> Rmin x z <= Rmin y z

forall x y z : R, x <= y -> Rmin x z <= Rmin y z
intros; do 2 (apply Rmin_case_strong; intro); eauto using Rle_trans, Rle_refl. Qed. (*********)

forall x y z : R, x <= y -> Rmin z x <= Rmin z y

forall x y z : R, x <= y -> Rmin z x <= Rmin z y
intros; do 2 (apply Rmin_case_strong; intro); eauto using Rle_trans, Rle_refl. Qed. (*********)

forall x y : R, Rmin x y = Rmin y x

forall x y : R, Rmin x y = Rmin y x
intros; unfold Rmin; case (Rle_dec x y); case (Rle_dec y x); intros; try reflexivity || (apply Rle_antisym; assumption || auto with real). Qed. (*********)

forall x y : posreal, 0 < Rmin x y

forall x y : posreal, 0 < Rmin x y
intros; apply Rmin_Rgt_r; split; [ apply (cond_pos x) | apply (cond_pos y) ]. Qed. (*********)

forall x y : R, 0 < x -> 0 < y -> 0 < Rmin x y

forall x y : R, 0 < x -> 0 < y -> 0 < Rmin x y
x, y:R
H:0 < x
H0:0 < y

0 < (if Rle_dec x y then x else y)
case (Rle_dec x y); intro; assumption. Qed. (*********)

forall x y z : R, z <= x -> z <= y -> z <= Rmin x y

forall x y z : R, z <= x -> z <= y -> z <= Rmin x y
intros; unfold Rmin; case (Rle_dec x y); intro; assumption. Qed. (*********)

forall x y z : R, z < x -> z < y -> z < Rmin x y

forall x y z : R, z < x -> z < y -> z < Rmin x y
intros; unfold Rmin; case (Rle_dec x y); intro; assumption. Qed. (*******************************)

Rmax

(*******************************)

(*********)
Definition Rmax (x y:R) : R :=
  match Rle_dec x y with
    | left _ => y
    | right _ => x
  end.

(*********)

forall (r1 r2 : R) (P : R -> Type), P r1 -> P r2 -> P (Rmax r1 r2)

forall (r1 r2 : R) (P : R -> Type), P r1 -> P r2 -> P (Rmax r1 r2)
intros r1 r2 P H1 H2; unfold Rmax; case (Rle_dec r1 r2); auto. Qed. (*********)

forall (r1 r2 : R) (P : R -> Type), (r2 <= r1 -> P r1) -> (r1 <= r2 -> P r2) -> P (Rmax r1 r2)

forall (r1 r2 : R) (P : R -> Type), (r2 <= r1 -> P r1) -> (r1 <= r2 -> P r2) -> P (Rmax r1 r2)
intros r1 r2 P H1 H2; unfold Rmax; case (Rle_dec r1 r2); auto with real. Qed. (*********)

forall r1 r2 r : R, r <= Rmax r1 r2 <-> r <= r1 \/ r <= r2

forall r1 r2 r : R, r <= Rmax r1 r2 <-> r <= r1 \/ r <= r2
r1, r2, r:R

r <= Rmax r1 r2 -> r <= r1 \/ r <= r2
r1, r2, r:R
r <= r1 \/ r <= r2 -> r <= Rmax r1 r2
r1, r2, r:R

r <= r1 \/ r <= r2 -> r <= Rmax r1 r2
r1, r2, r:R
r0:r1 <= r2
H:r <= r1

r <= r2
r1, r2, r:R
Hnle:~ r1 <= r2
H:r <= r2
r <= r1
r1, r2, r:R
Hnle:~ r1 <= r2
H:r <= r2

r <= r1
generalize (Rnot_le_lt r1 r2 Hnle); clear Hnle; intro; unfold Rgt in H0; apply (Rlt_le r r1 (Rle_lt_trans r r2 r1 H H0)). Qed.

forall x y : R, Rmax x y = Rmax y x

forall x y : R, Rmax x y = Rmax y x
intros p q; unfold Rmax; case (Rle_dec p q); case (Rle_dec q p); auto; intros H1 H2; apply Rle_antisym; auto with real. Qed. (* begin hide *) Notation RmaxSym := Rmax_comm (only parsing). (* end hide *) (*********)

forall x y : R, x <= Rmax x y

forall x y : R, x <= Rmax x y
intros; unfold Rmax; case (Rle_dec x y); intro H1; [ assumption | auto with real ]. Qed. (*********)

forall x y : R, y <= Rmax x y

forall x y : R, y <= Rmax x y
intros; unfold Rmax; case (Rle_dec x y); intro H1; [ right; reflexivity | auto with real ]. Qed. (* begin hide *) Notation RmaxLess1 := Rmax_l (only parsing). Notation RmaxLess2 := Rmax_r (only parsing). (* end hide *) (*********)

forall x y : R, y <= x -> Rmax x y = x

forall x y : R, y <= x -> Rmax x y = x
intros; apply Rmax_case_strong; auto using Rle_antisym. Qed. (*********)

forall x y : R, x <= y -> Rmax x y = y

forall x y : R, x <= y -> Rmax x y = y
intros; apply Rmax_case_strong; auto using Rle_antisym. Qed. (*********)

forall x y z : R, x <= y -> Rmax x z <= Rmax y z

forall x y z : R, x <= y -> Rmax x z <= Rmax y z
intros; do 2 (apply Rmax_case_strong; intro); eauto using Rle_trans, Rle_refl. Qed. (*********)

forall x y z : R, x <= y -> Rmax z x <= Rmax z y

forall x y z : R, x <= y -> Rmax z x <= Rmax z y
intros; do 2 (apply Rmax_case_strong; intro); eauto using Rle_trans, Rle_refl. Qed. (*********)

forall p q r : R, 0 <= r -> Rmax (r * p) (r * q) = r * Rmax p q

forall p q r : R, 0 <= r -> Rmax (r * p) (r * q) = r * Rmax p q
p, q, r:R
H:0 <= r

(if Rle_dec (r * p) (r * q) then r * q else r * p) = r * (if Rle_dec p q then q else p)
p, q, r:R
H:0 <= r
H1:~ r * p <= r * q
H2:p <= q

r * p = r * q
p, q, r:R
H:0 <= r
H1:r * p <= r * q
H2:~ p <= q
r * q = r * p
p, q, r:R
H:0 <= r
H1:~ r * p <= r * q
H2:p <= q
E1:0 < r

r * p = r * q
p, q, r:R
H:0 <= r
H1:~ r * p <= r * q
H2:p <= q
E1:0 = r
r * p = r * q
p, q, r:R
H:0 <= r
H1:r * p <= r * q
H2:~ p <= q
r * q = r * p
p, q, r:R
H:0 <= r
H1:~ r * p <= r * q
H2:p <= q
E1:0 = r

r * p = r * q
p, q, r:R
H:0 <= r
H1:r * p <= r * q
H2:~ p <= q
r * q = r * p
p, q, r:R
H:0 <= r
H1:r * p <= r * q
H2:~ p <= q

r * q = r * p
p, q, r:R
H:0 <= r
H1:r * p <= r * q
H2:~ p <= q
E1:0 < r

r * q = r * p
p, q, r:R
H:0 <= r
H1:r * p <= r * q
H2:~ p <= q
E1:0 = r
r * q = r * p
p, q, r:R
H:0 <= r
H1:r * p <= r * q
H2:~ p <= q
E1:0 < r

p <= q
p, q, r:R
H:0 <= r
H1:r * p <= r * q
H2:~ p <= q
E1:0 = r
r * q = r * p
p, q, r:R
H:0 <= r
H1:r * p <= r * q
H2:~ p <= q
E1:0 = r

r * q = r * p
rewrite <- E1; repeat rewrite Rmult_0_l; auto. Qed. (*********)

forall x y : negreal, Rmax x y < 0

forall x y : negreal, Rmax x y < 0
intros; unfold Rmax; case (Rle_dec x y); intro; [ apply (cond_neg y) | apply (cond_neg x) ]. Qed. (*********)

forall x y z : R, x <= z -> y <= z -> Rmax x y <= z

forall x y z : R, x <= z -> y <= z -> Rmax x y <= z
intros; unfold Rmax; case (Rle_dec x y); intro; assumption. Qed. (*********)

forall x y z : R, x < z -> y < z -> Rmax x y < z

forall x y z : R, x < z -> y < z -> Rmax x y < z
intros; unfold Rmax; case (Rle_dec x y); intro; assumption. Qed.

forall x y z : R, Rmax x y < z <-> x < z /\ y < z

forall x y z : R, Rmax x y < z <-> x < z /\ y < z
x, y, z:R

Rmax x y < z -> x < z /\ y < z
x, y, z:R
x < z /\ y < z -> Rmax x y < z
x, y, z:R

x <= y -> y < z -> x < z /\ y < z
x, y, z:R
~ x <= y -> x < z -> x < z /\ y < z
x, y, z:R
x < z /\ y < z -> Rmax x y < z
x, y, z:R

~ x <= y -> x < z -> x < z /\ y < z
x, y, z:R
x < z /\ y < z -> Rmax x y < z
x, y, z:R

x < z /\ y < z -> Rmax x y < z
intros [h h']; apply Rmax_lub_lt; assumption. Qed. (*********)

forall x y : R, x < 0 -> y < 0 -> Rmax x y < 0

forall x y : R, x < 0 -> y < 0 -> Rmax x y < 0
x, y:R
H:x < 0
H0:y < 0

(if Rle_dec x y then y else x) < 0
case (Rle_dec x y); intro; assumption. Qed. (*******************************)

Rabsolu

(*******************************)

(*********)

forall r : R, {r < 0} + {r >= 0}

forall r : R, {r < 0} + {r >= 0}
r:R
H:0 <= r

{r < 0} + {r >= 0}
r:R
H:~ 0 <= r
{r < 0} + {r >= 0}
r:R
H:~ 0 <= r

{r < 0} + {r >= 0}
left; fold (0 > r); apply (Rnot_le_lt 0 r H). Qed. (*********) Definition Rabs r : R := match Rcase_abs r with | left _ => - r | right _ => r end. (*********)

Rabs 0 = 0

Rabs 0 = 0
r:0 < 0

- 0 = 0
generalize (Rlt_irrefl 0); intro; exfalso; auto. Qed.

Rabs 1 = 1

Rabs 1 = 1

1 < 0 -> - (1) = 1
intros H; absurd (1 < 0); auto with real. Qed. (*********)

forall r : R, r <> 0 -> Rabs r <> 0

forall r : R, r <> 0 -> Rabs r <> 0
r:R
H:r <> 0
r0:r < 0

- r <> 0
apply Ropp_neq_0_compat; auto. Qed. (*********)

forall r : R, r < 0 -> Rabs r = - r

forall r : R, r < 0 -> Rabs r = - r
r:R
H:r < 0
r0:r >= 0

~ r >= 0
r:R
H:r < 0
r0:r >= 0
r >= 0
r:R
H:r < 0
r0:r >= 0

r >= 0
assumption. Qed. (*********)

forall r : R, r >= 0 -> Rabs r = r

forall r : R, r >= 0 -> Rabs r = r
r:R
H:r >= 0
Hlt:r < 0

- r = r
r:R
H, Hge:r >= 0
r = r
r:R
H:r >= 0
Hlt:r < 0

~ r >= 0
r:R
H:r >= 0
Hlt:r < 0
r >= 0
r:R
H, Hge:r >= 0
r = r
r:R
H:r >= 0
Hlt:r < 0

r >= 0
r:R
H, Hge:r >= 0
r = r
r:R
H, Hge:r >= 0

r = r
trivial. Qed.

forall a : R, a <= 0 -> Rabs a = - a

forall a : R, a <= 0 -> Rabs a = - a
a:R
H:a <= 0
H1:a < 0

Rabs a = - a
a:R
H:a <= 0
H1:a = 0
Rabs a = - a
a:R
H:a <= 0
H1:a = 0

Rabs a = - a
rewrite H1; simpl; rewrite Rabs_right; auto with real. Qed. (*********)

forall x : R, 0 <= Rabs x

forall x : R, 0 <= Rabs x
x:R
Hlt:x < 0

0 <= - x
x:R
Hge:x >= 0
0 <= x
x:R
Hge:x >= 0

0 <= x
apply Rge_le; assumption. Qed.

forall x : R, x <= Rabs x

forall x : R, x <= Rabs x
x:R
r:x < 0

x <= - x
apply Rminus_le; rewrite <- Rplus_0_r; unfold Rminus; rewrite Ropp_involutive; auto with real. Qed. Definition RRle_abs := Rle_abs.

forall a b : R, - b <= a <= b -> Rabs a <= b

forall a b : R, - b <= a <= b -> Rabs a <= b
a, b:R

a < 0 -> - b <= a <= b -> - a <= b
a, b:R
a >= 0 -> - b <= a <= b -> a <= b
a, b:R

a >= 0 -> - b <= a <= b -> a <= b
intros _ [_ it]; exact it. Qed. (*********)

forall x : R, 0 <= x -> Rabs x = x

forall x : R, 0 <= x -> Rabs x = x
intros; unfold Rabs; case (Rcase_abs x) as [Hlt|Hge]; [ generalize (Rgt_not_le 0 x Hlt); intro; exfalso; auto | trivial ]. Qed. (*********)

forall x : R, Rabs (Rabs x) = Rabs x

forall x : R, Rabs (Rabs x) = Rabs x
intro; apply (Rabs_pos_eq (Rabs x) (Rabs_pos x)). Qed. (*********)

forall x : R, x <> 0 -> 0 < Rabs x

forall x : R, x <> 0 -> 0 < Rabs x
x:R
H:x <> 0
Heq:0 = Rabs x

0 < Rabs x
apply Rabs_no_R0 in H; symmetry in Heq; contradiction. Qed. (*********)

forall x y : R, Rabs (x - y) = Rabs (y - x)

forall x y : R, Rabs (x - y) = Rabs (y - x)
x, y:R
Hlt:x - y < 0
Hlt':y - x < 0

- (x - y) = - (y - x)
x, y:R
Hlt:x - y < 0
Hge':y - x >= 0
- (x - y) = y - x
x, y:R
Hge:x - y >= 0
Hlt':y - x < 0
x - y = - (y - x)
x, y:R
Hge:x - y >= 0
Hge':y - x >= 0
x - y = y - x
x, y:R
Hlt:x - y < 0
Hge':y - x >= 0

- (x - y) = y - x
x, y:R
Hge:x - y >= 0
Hlt':y - x < 0
x - y = - (y - x)
x, y:R
Hge:x - y >= 0
Hge':y - x >= 0
x - y = y - x
x, y:R
Hge:x - y >= 0
Hlt':y - x < 0

x - y = - (y - x)
x, y:R
Hge:x - y >= 0
Hge':y - x >= 0
x - y = y - x
x, y:R
Hge:x - y >= 0
Hge':y - x >= 0

x - y = y - x
x, y:R
H:x - y > 0
H0:y - x > 0

x - y = y - x
x, y:R
H:x - y > 0
H0:y - x = 0
x - y = y - x
x, y:R
H:x - y = 0
H0:y - x > 0
x - y = y - x
x, y:R
H:x - y = 0
H0:y - x = 0
x - y = y - x
x, y:R
H:x - y > 0
H0:y - x = 0

x - y = y - x
x, y:R
H:x - y = 0
H0:y - x > 0
x - y = y - x
x, y:R
H:x - y = 0
H0:y - x = 0
x - y = y - x
x, y:R
H:x - y = 0
H0:y - x > 0

x - y = y - x
x, y:R
H:x - y = 0
H0:y - x = 0
x - y = y - x
x, y:R
H:x - y = 0
H0:y - x = 0

x - y = y - x
apply Rminus_diag_uniq in H0 as ->; trivial. Qed. (*********)

forall x y : R, Rabs (x * y) = Rabs x * Rabs y

forall x y : R, Rabs (x * y) = Rabs x * Rabs y
x, y:R
Hlt:x * y < 0
Hltx:x < 0
Hlty:y < 0

- (x * y) = - x * - y
x, y:R
Hlt:x * y < 0
Hltx:x < 0
Hgey:y >= 0
- (x * y) = - x * y
x, y:R
Hlt:x * y < 0
Hgex:x >= 0
Hlty:y < 0
- (x * y) = x * - y
x, y:R
Hlt:x * y < 0
Hgex:x >= 0
Hgey:y >= 0
- (x * y) = x * y
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hlty:y < 0
x * y = - x * - y
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hgey:y >= 0
x * y = - x * y
x, y:R
Hge:x * y >= 0
Hgex:x >= 0
Hlty:y < 0
x * y = x * - y
x, y:R
Hlt:x * y < 0
Hltx:x < 0
Hlty:~ x * y < x * 0

- (x * y) = - x * - y
x, y:R
Hlt:x * y < 0
Hltx:x < 0
Hgey:y >= 0
- (x * y) = - x * y
x, y:R
Hlt:x * y < 0
Hgex:x >= 0
Hlty:y < 0
- (x * y) = x * - y
x, y:R
Hlt:x * y < 0
Hgex:x >= 0
Hgey:y >= 0
- (x * y) = x * y
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hlty:y < 0
x * y = - x * - y
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hgey:y >= 0
x * y = - x * y
x, y:R
Hge:x * y >= 0
Hgex:x >= 0
Hlty:y < 0
x * y = x * - y
x, y:R
Hlt:x * y < 0
Hltx:x < 0
Hgey:y >= 0

- (x * y) = - x * y
x, y:R
Hlt:x * y < 0
Hgex:x >= 0
Hlty:y < 0
- (x * y) = x * - y
x, y:R
Hlt:x * y < 0
Hgex:x >= 0
Hgey:y >= 0
- (x * y) = x * y
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hlty:y < 0
x * y = - x * - y
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hgey:y >= 0
x * y = - x * y
x, y:R
Hge:x * y >= 0
Hgex:x >= 0
Hlty:y < 0
x * y = x * - y
x, y:R
Hlt:x * y < 0
Hgex:x >= 0
Hlty:y < 0

- (x * y) = x * - y
x, y:R
Hlt:x * y < 0
Hgex:x >= 0
Hgey:y >= 0
- (x * y) = x * y
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hlty:y < 0
x * y = - x * - y
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hgey:y >= 0
x * y = - x * y
x, y:R
Hge:x * y >= 0
Hgex:x >= 0
Hlty:y < 0
x * y = x * - y
x, y:R
Hlt:x * y < 0
Hgex:x >= 0
Hgey:y >= 0

- (x * y) = x * y
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hlty:y < 0
x * y = - x * - y
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hgey:y >= 0
x * y = - x * y
x, y:R
Hge:x * y >= 0
Hgex:x >= 0
Hlty:y < 0
x * y = x * - y
x, y:R
Hlt:x * y < 0
H:x > 0
H0:y > 0

- (x * y) = x * y
x:R
Hlt:x * 0 < 0
H:x > 0
- (x * 0) = x * 0
y:R
Hlt:0 * y < 0
H:y > 0
- (0 * y) = 0 * y
Hlt:0 * 0 < 0
- (0 * 0) = 0 * 0
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hlty:y < 0
x * y = - x * - y
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hgey:y >= 0
x * y = - x * y
x, y:R
Hge:x * y >= 0
Hgex:x >= 0
Hlty:y < 0
x * y = x * - y
x, y:R
Hlt:x * y < 0
H:x > 0
H0:~ x * y < x * 0

- (x * y) = x * y
x:R
Hlt:x * 0 < 0
H:x > 0
- (x * 0) = x * 0
y:R
Hlt:0 * y < 0
H:y > 0
- (0 * y) = 0 * y
Hlt:0 * 0 < 0
- (0 * 0) = 0 * 0
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hlty:y < 0
x * y = - x * - y
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hgey:y >= 0
x * y = - x * y
x, y:R
Hge:x * y >= 0
Hgex:x >= 0
Hlty:y < 0
x * y = x * - y
x:R
Hlt:x * 0 < 0
H:x > 0

- (x * 0) = x * 0
y:R
Hlt:0 * y < 0
H:y > 0
- (0 * y) = 0 * y
Hlt:0 * 0 < 0
- (0 * 0) = 0 * 0
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hlty:y < 0
x * y = - x * - y
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hgey:y >= 0
x * y = - x * y
x, y:R
Hge:x * y >= 0
Hgex:x >= 0
Hlty:y < 0
x * y = x * - y
y:R
Hlt:0 * y < 0
H:y > 0

- (0 * y) = 0 * y
Hlt:0 * 0 < 0
- (0 * 0) = 0 * 0
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hlty:y < 0
x * y = - x * - y
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hgey:y >= 0
x * y = - x * y
x, y:R
Hge:x * y >= 0
Hgex:x >= 0
Hlty:y < 0
x * y = x * - y
Hlt:0 * 0 < 0

- (0 * 0) = 0 * 0
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hlty:y < 0
x * y = - x * - y
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hgey:y >= 0
x * y = - x * y
x, y:R
Hge:x * y >= 0
Hgex:x >= 0
Hlty:y < 0
x * y = x * - y
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hlty:y < 0

x * y = - x * - y
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hgey:y >= 0
x * y = - x * y
x, y:R
Hge:x * y >= 0
Hgex:x >= 0
Hlty:y < 0
x * y = x * - y
x, y:R
Hge:x * y >= 0
Hltx:x < 0
Hgey:y >= 0

x * y = - x * y
x, y:R
Hge:x * y >= 0
Hgex:x >= 0
Hlty:y < 0
x * y = x * - y
x, y:R
H:x * y > 0
Hltx:x < 0
Hgey:y >= 0

x * y = - x * y
x, y:R
H:x * y = 0
Hltx:x < 0
Hgey:y >= 0
x * y = - x * y
x, y:R
Hge:x * y >= 0
Hgex:x >= 0
Hlty:y < 0
x * y = x * - y
x, y:R
H:x * y > 0
Hltx:x < 0
H0:y > 0

x * y = - x * y
x, y:R
H:x * y > 0
Hltx:x < 0
H0:y = 0
x * y = - x * y
x, y:R
H:x * y = 0
Hltx:x < 0
Hgey:y >= 0
x * y = - x * y
x, y:R
Hge:x * y >= 0
Hgex:x >= 0
Hlty:y < 0
x * y = x * - y
x, y:R
H:x * y > 0
Hltx:~ 0 * y < x * y
H0:y > 0

x * y = - x * y
x, y:R
H:x * y > 0
Hltx:x < 0
H0:y = 0
x * y = - x * y
x, y:R
H:x * y = 0
Hltx:x < 0
Hgey:y >= 0
x * y = - x * y
x, y:R
Hge:x * y >= 0
Hgex:x >= 0
Hlty:y < 0
x * y = x * - y
x, y:R
H:x * y > 0
Hltx:x < 0
H0:y = 0

x * y = - x * y
x, y:R
H:x * y = 0
Hltx:x < 0
Hgey:y >= 0
x * y = - x * y
x, y:R
Hge:x * y >= 0
Hgex:x >= 0
Hlty:y < 0
x * y = x * - y
x, y:R
H:x * y = 0
Hltx:x < 0
Hgey:y >= 0

x * y = - x * y
x, y:R
Hge:x * y >= 0
Hgex:x >= 0
Hlty:y < 0
x * y = x * - y
x, y:R
Hge:x * y >= 0
Hgex:x >= 0
Hlty:y < 0

x * y = x * - y
x, y:R
H:x * y > 0
Hgex:x >= 0
Hlty:y < 0

x * y = x * - y
x, y:R
H:x * y = 0
Hgex:x >= 0
Hlty:y < 0
x * y = x * - y
x, y:R
H:x * y > 0
H0:x > 0
Hlty:y < 0

x * y = x * - y
x, y:R
H:x * y > 0
H0:x = 0
Hlty:y < 0
x * y = x * - y
x, y:R
H:x * y = 0
Hgex:x >= 0
Hlty:y < 0
x * y = x * - y
x, y:R
H:x * y > 0
H0:x > 0
Hlty:~ x * 0 < x * y

x * y = x * - y
x, y:R
H:x * y > 0
H0:x = 0
Hlty:y < 0
x * y = x * - y
x, y:R
H:x * y = 0
Hgex:x >= 0
Hlty:y < 0
x * y = x * - y
x, y:R
H:x * y > 0
H0:x = 0
Hlty:y < 0

x * y = x * - y
x, y:R
H:x * y = 0
Hgex:x >= 0
Hlty:y < 0
x * y = x * - y
x, y:R
H:x * y = 0
Hgex:x >= 0
Hlty:y < 0

x * y = x * - y
rewrite <- Ropp_mult_distr_r, H, Ropp_0; trivial. Qed. (*********)

forall r : R, r <> 0 -> Rabs (/ r) = / Rabs r

forall r : R, r <> 0 -> Rabs (/ r) = / Rabs r
r:R
Hlt:r < 0
Hlt':/ r < 0
H:r <> 0

- / r = / - r
r:R
Hlt:r < 0
Hge':/ r >= 0
H:r <> 0
/ r = / - r
r:R
Hge:r >= 0
Hlt':/ r < 0
H:r <> 0
- / r = / r
r:R
Hlt:r < 0
Hge':/ r >= 0
H:r <> 0

/ r = / - r
r:R
Hge:r >= 0
Hlt':/ r < 0
H:r <> 0
- / r = / r
r:R
Hlt:r < 0
Hge':/ r >= 0
H:r <> 0

/ r = - / r
r:R
Hge:r >= 0
Hlt':/ r < 0
H:r <> 0
- / r = / r
r:R
Hlt:r < 0
H0:/ r > 0
H:r <> 0

/ r = - / r
r:R
Hlt:r < 0
H:r <> 0
0 = - 0
r:R
Hge:r >= 0
Hlt':/ r < 0
H:r <> 0
- / r = / r
r:R
Hlt:r < 0
H:r <> 0

0 = - 0
r:R
Hge:r >= 0
Hlt':/ r < 0
H:r <> 0
- / r = / r
r:R
Hge:r >= 0
Hlt':/ r < 0
H:r <> 0

- / r = / r
r:R
H0:r > 0
Hlt':/ r < 0
H:r <> 0

- / r = / r
H:0 <> 0
Hlt':/ 0 < 0
- / 0 = / 0
H:0 <> 0
Hlt':/ 0 < 0

- / 0 = / 0
contradiction (refl_equal 0). Qed.

forall x : R, Rabs (- x) = Rabs x

forall x : R, Rabs (- x) = Rabs x
x:R

Rabs (-1 * x) = Rabs x
x:R

Rabs (-1) * Rabs x = Rabs x
x:R

1 * Rabs x = Rabs x
x:R
1 = Rabs (-1)
x:R

1 = Rabs (-1)
x:R

-1 < 0 -> 1 = - -1
x:R
-1 >= 0 -> 1 = -1
x:R

-1 >= 0 -> 1 = -1
x:R

-1 >= - 0 -> 1 = -1
x:R
H0:0 >= IPR 1

1 = -1
x:R
H0:0 >= IPR 1

0 < IPR 1
apply Rlt_0_1. Qed. (*********)

forall a b : R, Rabs (a + b) <= Rabs a + Rabs b

forall a b : R, Rabs (a + b) <= Rabs a + Rabs b
a, b:R
Hlt:a + b < 0
Hlta:a < 0
Hltb:b < 0

- (a + b) <= - a + - b
a, b:R
Hlt:a + b < 0
Hlta:a < 0
Hgeb:b >= 0
- (a + b) <= - a + b
a, b:R
Hlt:a + b < 0
Hgea:a >= 0
Hltb:b < 0
- (a + b) <= a + - b
a, b:R
Hlt:a + b < 0
Hgea:a >= 0
Hgeb:b >= 0
- (a + b) <= a + b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hltb:b < 0
a + b <= - a + - b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hgeb:b >= 0
a + b <= - a + b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hltb:b < 0
a + b <= a + - b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hgeb:b >= 0
a + b <= a + b
a, b:R
Hlt:a + b < 0
Hlta:a < 0
Hgeb:b >= 0

- (a + b) <= - a + b
a, b:R
Hlt:a + b < 0
Hgea:a >= 0
Hltb:b < 0
- (a + b) <= a + - b
a, b:R
Hlt:a + b < 0
Hgea:a >= 0
Hgeb:b >= 0
- (a + b) <= a + b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hltb:b < 0
a + b <= - a + - b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hgeb:b >= 0
a + b <= - a + b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hltb:b < 0
a + b <= a + - b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hgeb:b >= 0
a + b <= a + b
(**)
a, b:R
Hlt:a + b < 0
Hlta:a < 0
Hgeb:b >= 0
H:b > 0

- b < b \/ - b = b
a, b:R
Hlt:a + b < 0
Hlta:a < 0
Hgeb:b >= 0
H:b = 0
- b < b \/ - b = b
a, b:R
Hlt:a + b < 0
Hgea:a >= 0
Hltb:b < 0
- (a + b) <= a + - b
a, b:R
Hlt:a + b < 0
Hgea:a >= 0
Hgeb:b >= 0
- (a + b) <= a + b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hltb:b < 0
a + b <= - a + - b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hgeb:b >= 0
a + b <= - a + b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hltb:b < 0
a + b <= a + - b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hgeb:b >= 0
a + b <= a + b
a, b:R
Hlt:a + b < 0
Hlta:a < 0
Hgeb:b >= 0
H:b = 0

- b < b \/ - b = b
a, b:R
Hlt:a + b < 0
Hgea:a >= 0
Hltb:b < 0
- (a + b) <= a + - b
a, b:R
Hlt:a + b < 0
Hgea:a >= 0
Hgeb:b >= 0
- (a + b) <= a + b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hltb:b < 0
a + b <= - a + - b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hgeb:b >= 0
a + b <= - a + b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hltb:b < 0
a + b <= a + - b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hgeb:b >= 0
a + b <= a + b
a, b:R
Hlt:a + b < 0
Hgea:a >= 0
Hltb:b < 0

- (a + b) <= a + - b
a, b:R
Hlt:a + b < 0
Hgea:a >= 0
Hgeb:b >= 0
- (a + b) <= a + b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hltb:b < 0
a + b <= - a + - b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hgeb:b >= 0
a + b <= - a + b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hltb:b < 0
a + b <= a + - b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hgeb:b >= 0
a + b <= a + b
(**)
a, b:R
Hlt:a + b < 0
Hgea:a >= 0
Hltb:b < 0
H:a > 0

- a < a \/ - a = a
a, b:R
Hlt:a + b < 0
Hgea:a >= 0
Hltb:b < 0
H:a = 0
- a < a \/ - a = a
a, b:R
Hlt:a + b < 0
Hgea:a >= 0
Hgeb:b >= 0
- (a + b) <= a + b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hltb:b < 0
a + b <= - a + - b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hgeb:b >= 0
a + b <= - a + b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hltb:b < 0
a + b <= a + - b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hgeb:b >= 0
a + b <= a + b
a, b:R
Hlt:a + b < 0
Hgea:a >= 0
Hltb:b < 0
H:a = 0

- a < a \/ - a = a
a, b:R
Hlt:a + b < 0
Hgea:a >= 0
Hgeb:b >= 0
- (a + b) <= a + b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hltb:b < 0
a + b <= - a + - b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hgeb:b >= 0
a + b <= - a + b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hltb:b < 0
a + b <= a + - b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hgeb:b >= 0
a + b <= a + b
a, b:R
Hlt:a + b < 0
Hgea:a >= 0
Hgeb:b >= 0

- (a + b) <= a + b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hltb:b < 0
a + b <= - a + - b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hgeb:b >= 0
a + b <= - a + b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hltb:b < 0
a + b <= a + - b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hgeb:b >= 0
a + b <= a + b
(**)
a, b:R
Hlt:a + b < 0
Hgea:a >= 0
Hgeb:b >= 0
H:a + b > 0

False
a, b:R
Hlt:a + b < 0
Hgea:a >= 0
Hgeb:b >= 0
H:a + b = 0
False
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hltb:b < 0
a + b <= - a + - b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hgeb:b >= 0
a + b <= - a + b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hltb:b < 0
a + b <= a + - b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hgeb:b >= 0
a + b <= a + b
a, b:R
Hlt:a + b < 0
Hgea:a >= 0
Hgeb:b >= 0
H:a + b = 0

False
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hltb:b < 0
a + b <= - a + - b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hgeb:b >= 0
a + b <= - a + b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hltb:b < 0
a + b <= a + - b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hgeb:b >= 0
a + b <= a + b
a, b:R
Hlt:a + b < 0
Hgea:a >= 0
Hgeb:b >= 0
H:a + b = 0

a + b <> 0
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hltb:b < 0
a + b <= - a + - b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hgeb:b >= 0
a + b <= - a + b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hltb:b < 0
a + b <= a + - b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hgeb:b >= 0
a + b <= a + b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hltb:b < 0

a + b <= - a + - b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hgeb:b >= 0
a + b <= - a + b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hltb:b < 0
a + b <= a + - b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hgeb:b >= 0
a + b <= a + b
(**)
a, b:R
H:a + b > 0
Hlta:a < 0
Hltb:b < 0
H0:a + b < 0

False
a, b:R
H:a + b = 0
Hlta:a < 0
Hltb:b < 0
H0:a + b < 0
False
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hgeb:b >= 0
a + b <= - a + b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hltb:b < 0
a + b <= a + - b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hgeb:b >= 0
a + b <= a + b
a, b:R
H:a + b = 0
Hlta:a < 0
Hltb:b < 0
H0:a + b < 0

False
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hgeb:b >= 0
a + b <= - a + b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hltb:b < 0
a + b <= a + - b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hgeb:b >= 0
a + b <= a + b
a, b:R
Hge:a + b >= 0
Hlta:a < 0
Hgeb:b >= 0

a + b <= - a + b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hltb:b < 0
a + b <= a + - b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hgeb:b >= 0
a + b <= a + b
(**)
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hltb:b < 0

a + b <= a + - b
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hgeb:b >= 0
a + b <= a + b
(**)
a, b:R
Hge:a + b >= 0
Hgea:a >= 0
Hgeb:b >= 0

a + b <= a + b
(**) unfold Rle; right; reflexivity. Qed. (*********)

forall a b : R, Rabs a - Rabs b <= Rabs (a - b)

forall a b : R, Rabs a - Rabs b <= Rabs (a - b)
a, b:R

Rabs (a + 0) <= Rabs b + Rabs (a + - b)
a, b:R
Rabs (a + 0) = Rabs a
a, b:R

Rabs (b + (a + - b)) <= Rabs b + Rabs (a + - b)
a, b:R
Rabs (a + 0) = Rabs a
a, b:R

Rabs (a + 0) = Rabs a
rewrite (proj1 (Rplus_ne a)); trivial. Qed. (* ||a|-|b||<=|a-b| *)

forall a b : R, Rabs (Rabs a - Rabs b) <= Rabs (a - b)

forall a b : R, Rabs (Rabs a - Rabs b) <= Rabs (a - b)

(forall a b : R, Rabs b <= Rabs a -> Rabs (Rabs a - Rabs b) <= Rabs (a - b)) -> forall a b : R, Rabs (Rabs a - Rabs b) <= Rabs (a - b)

forall a b : R, Rabs b <= Rabs a -> Rabs (Rabs a - Rabs b) <= Rabs (a - b)
H:forall a0 b0 : R, Rabs b0 <= Rabs a0 -> Rabs (Rabs a0 - Rabs b0) <= Rabs (a0 - b0)
a, b:R
Hlt:Rabs a < Rabs b

Rabs (Rabs a - Rabs b) <= Rabs (a - b)
H:forall a0 b0 : R, Rabs b0 <= Rabs a0 -> Rabs (Rabs a0 - Rabs b0) <= Rabs (a0 - b0)
a, b:R
Heq:Rabs a = Rabs b
Rabs (Rabs a - Rabs b) <= Rabs (a - b)
H:forall a0 b0 : R, Rabs b0 <= Rabs a0 -> Rabs (Rabs a0 - Rabs b0) <= Rabs (a0 - b0)
a, b:R
Hgt:Rabs a > Rabs b
Rabs (Rabs a - Rabs b) <= Rabs (a - b)

forall a b : R, Rabs b <= Rabs a -> Rabs (Rabs a - Rabs b) <= Rabs (a - b)
H:forall a0 b0 : R, Rabs b0 <= Rabs a0 -> Rabs (Rabs a0 - Rabs b0) <= Rabs (a0 - b0)
a, b:R
Hlt:Rabs a < Rabs b

Rabs (Rabs b - Rabs a) <= Rabs (b - a)
H:forall a0 b0 : R, Rabs b0 <= Rabs a0 -> Rabs (Rabs a0 - Rabs b0) <= Rabs (a0 - b0)
a, b:R
Heq:Rabs a = Rabs b
Rabs (Rabs a - Rabs b) <= Rabs (a - b)
H:forall a0 b0 : R, Rabs b0 <= Rabs a0 -> Rabs (Rabs a0 - Rabs b0) <= Rabs (a0 - b0)
a, b:R
Hgt:Rabs a > Rabs b
Rabs (Rabs a - Rabs b) <= Rabs (a - b)

forall a b : R, Rabs b <= Rabs a -> Rabs (Rabs a - Rabs b) <= Rabs (a - b)
H:forall a0 b0 : R, Rabs b0 <= Rabs a0 -> Rabs (Rabs a0 - Rabs b0) <= Rabs (a0 - b0)
a, b:R
Heq:Rabs a = Rabs b

Rabs (Rabs a - Rabs b) <= Rabs (a - b)
H:forall a0 b0 : R, Rabs b0 <= Rabs a0 -> Rabs (Rabs a0 - Rabs b0) <= Rabs (a0 - b0)
a, b:R
Hgt:Rabs a > Rabs b
Rabs (Rabs a - Rabs b) <= Rabs (a - b)

forall a b : R, Rabs b <= Rabs a -> Rabs (Rabs a - Rabs b) <= Rabs (a - b)
H:forall a0 b0 : R, Rabs b0 <= Rabs a0 -> Rabs (Rabs a0 - Rabs b0) <= Rabs (a0 - b0)
a, b:R
Hgt:Rabs a > Rabs b

Rabs (Rabs a - Rabs b) <= Rabs (a - b)

forall a b : R, Rabs b <= Rabs a -> Rabs (Rabs a - Rabs b) <= Rabs (a - b)

forall a b : R, Rabs b <= Rabs a -> Rabs (Rabs a - Rabs b) <= Rabs (a - b)
a, b:R
H:Rabs b <= Rabs a

Rabs a - Rabs b <= Rabs (a - b)
a, b:R
H:Rabs b <= Rabs a
Rabs a - Rabs b = Rabs (Rabs a - Rabs b)
a, b:R
H:Rabs b <= Rabs a

Rabs a - Rabs b = Rabs (Rabs a - Rabs b)
rewrite (Rabs_right (Rabs a - Rabs b)); [ reflexivity | apply Rle_ge; apply Rplus_le_reg_l with (Rabs b); rewrite Rplus_0_r; replace (Rabs b + (Rabs a - Rabs b)) with (Rabs a); [ assumption | ring ] ]. Qed. (*********)

forall x a : R, x < a -> - a < x -> Rabs x < a

forall x a : R, x < a -> - a < x -> Rabs x < a
x, a:R
H:x < a
H0:- a < x
r:x < 0

- x < a
x, a:R
H:x < a
H0:- a < x
r:x >= 0
x < a
x, a:R
H:x < a
H0:- a < x
r:x >= 0

x < a
assumption. Qed. (*********)

forall x a : R, Rabs x < a -> x < a /\ - a < x

forall x a : R, Rabs x < a -> x < a /\ - a < x
x:R
Hlt:x < 0
a:R
H:- x < a

x < a /\ - a < x
x:R
Hge:x >= 0
a:R
H:x < a
x < a /\ - a < x
x:R
Hlt:x < 0
a:R
H:- x < a
H0:0 < - x
H1:0 < a

x < a
x:R
Hlt:x < 0
a:R
H:- x < a
H0:0 < - x
H1:0 < a
- a < x
x:R
Hge:x >= 0
a:R
H:x < a
x < a /\ - a < x
x:R
Hlt:x < 0
a:R
H:- x < a
H0:0 < - x
H1:0 < a

- a < x
x:R
Hge:x >= 0
a:R
H:x < a
x < a /\ - a < x
x:R
Hge:x >= 0
a:R
H:x < a

x < a /\ - a < x
fold (a > x) in H; generalize (Rgt_ge_trans a x 0 H Hge); intro; generalize (Ropp_lt_gt_0_contravar a H0); intro; fold (0 > - a); generalize (Rge_gt_trans x 0 (- a) Hge H1); unfold Rgt; intro; split; assumption. Qed.

forall p q r : R, p <= q -> q <= r -> Rabs q <= Rmax (Rabs p) (Rabs r)

forall p q r : R, p <= q -> q <= r -> Rabs q <= Rmax (Rabs p) (Rabs r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:0 <= p

Rabs q <= Rmax (Rabs p) (Rabs r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
Rabs q <= Rmax (Rabs p) (Rabs r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:0 <= p

q <= Rmax p r
p, q, r:R
H':p <= q
H'0:q <= r
H'1:0 <= p
r >= 0
p, q, r:R
H':p <= q
H'0:q <= r
H'1:0 <= p
q >= 0
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
Rabs q <= Rmax (Rabs p) (Rabs r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:0 <= p

r <= Rmax p r
p, q, r:R
H':p <= q
H'0:q <= r
H'1:0 <= p
r >= 0
p, q, r:R
H':p <= q
H'0:q <= r
H'1:0 <= p
q >= 0
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
Rabs q <= Rmax (Rabs p) (Rabs r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:0 <= p

r >= 0
p, q, r:R
H':p <= q
H'0:q <= r
H'1:0 <= p
q >= 0
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
Rabs q <= Rmax (Rabs p) (Rabs r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:0 <= p

q >= 0
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
Rabs q <= Rmax (Rabs p) (Rabs r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0

Rabs q <= Rmax (Rabs p) (Rabs r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0

Rabs q <= Rmax (- p) (Rabs r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
H'2:0 <= q

Rabs q <= Rmax (- p) (Rabs r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
H'2:q < 0
Rabs q <= Rmax (- p) (Rabs r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
H'2:0 <= q

q <= Rmax (- p) r
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
H'2:0 <= q
r >= 0
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
H'2:q < 0
Rabs q <= Rmax (- p) (Rabs r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
H'2:0 <= q

r <= Rmax (- p) r
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
H'2:0 <= q
r >= 0
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
H'2:q < 0
Rabs q <= Rmax (- p) (Rabs r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
H'2:0 <= q

r >= 0
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
H'2:q < 0
Rabs q <= Rmax (- p) (Rabs r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
H'2:q < 0

Rabs q <= Rmax (- p) (Rabs r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
H'2:q < 0

- q <= Rmax (- p) (Rabs r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
H'2:q < 0
H'3:0 <= r

- q <= Rmax (- p) (Rabs r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
H'2:q < 0
H'3:r < 0
- q <= Rmax (- p) (Rabs r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
H'2:q < 0
H'3:0 <= r

- q <= Rmax (- p) r
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
H'2:q < 0
H'3:r < 0
- q <= Rmax (- p) (Rabs r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
H'2:q < 0
H'3:0 <= r

- p <= Rmax (- p) r
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
H'2:q < 0
H'3:r < 0
- q <= Rmax (- p) (Rabs r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
H'2:q < 0
H'3:r < 0

- q <= Rmax (- p) (Rabs r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
H'2:q < 0
H'3:r < 0

- q <= Rmax (- p) (- r)
p, q, r:R
H':p <= q
H'0:q <= r
H'1:p < 0
H'2:q < 0
H'3:r < 0

- p <= Rmax (- p) (- r)
apply RmaxLess1; auto. Qed.

forall z : Z, Rabs (IZR z) = IZR (Z.abs z)

forall z : Z, Rabs (IZR z) = IZR (Z.abs z)
z:Z

Rabs 0 = 0
z:Z
forall p : positive, Rabs (IZR (Z.pos p)) = IZR (Z.pos p)
z:Z
forall p : positive, Rabs (IZR (Z.neg p)) = IZR (Z.pos p)
z:Z

forall p : positive, Rabs (IZR (Z.pos p)) = IZR (Z.pos p)
z:Z
forall p : positive, Rabs (IZR (Z.neg p)) = IZR (Z.pos p)
z:Z

forall p : positive, Rabs (IZR (Z.neg p)) = IZR (Z.pos p)
z:Z

forall p : positive, Rabs (- IPR p) = IZR (Z.pos p)
z:Z
p0:positive

Rabs (IPR p0) = IZR (Z.pos p0)
now apply Rabs_pos_eq, (IZR_le 0). Qed.

forall z : Z, IZR (Z.abs z) = Rabs (IZR z)

forall z : Z, IZR (Z.abs z) = Rabs (IZR z)
z:Z

IZR (Z.abs z) = Rabs (IZR z)
now rewrite Rabs_Zabs. Qed.

forall x y : R, - Rmax x y = Rmin (- x) (- y)
x, y:R

y <= x -> - x = Rmin (- x) (- y)
x, y:R
x <= y -> - y = Rmin (- x) (- y)
x, y:R

x <= y -> - y = Rmin (- x) (- y)
now intros w; rewrite Rmin_right; [ | apply Rge_le, Ropp_le_ge_contravar]. Qed.

forall x y : R, - Rmin x y = Rmax (- x) (- y)
x, y:R

x <= y -> - x = Rmax (- x) (- y)
x, y:R
y <= x -> - y = Rmax (- x) (- y)
x, y:R

y <= x -> - y = Rmax (- x) (- y)
now intros w; rewrite Rmax_right; [ | apply Rge_le, Ropp_le_ge_contravar]. Qed.

forall a b c : R, Rmax a (Rmax b c) = Rmax (Rmax a b) c

forall a b c : R, Rmax a (Rmax b c) = Rmax (Rmax a b) c
a, b, c:R

Rmax a (Rmax b c) = Rmax (Rmax a b) c
unfold Rmax; destruct (Rle_dec b c); destruct (Rle_dec a b); destruct (Rle_dec a c); destruct (Rle_dec b c); auto with real; match goal with | id : ~ ?x <= ?y, id2 : ?x <= ?z |- _ => case id; apply Rle_trans with z; auto with real | id : ~ ?x <= ?y, id2 : ~ ?z <= ?x |- _ => case id; apply Rle_trans with z; auto with real end. Qed.

forall a b : R, Rmin a b <= Rmax a b

forall a b : R, Rmin a b <= Rmax a b
a, b:R
r:a <= b

Rmin a b <= Rmax a b
a, b:R
n:~ a <= b
Rmin a b <= Rmax a b
a, b:R
n:~ a <= b

Rmin a b <= Rmax a b
now rewrite Rmin_right, Rmax_left; assumption || apply Rlt_le, Rnot_le_gt. Qed.

forall x y z : R, Rmin x (Rmin y z) = Rmin (Rmin x y) z

forall x y z : R, Rmin x (Rmin y z) = Rmin (Rmin x y) z
a, b, c:R

Rmin a (Rmin b c) = Rmin (Rmin a b) c
unfold Rmin; destruct (Rle_dec b c); destruct (Rle_dec a b); destruct (Rle_dec a c); destruct (Rle_dec b c); auto with real; match goal with | id : ~ ?x <= ?y, id2 : ?x <= ?z |- _ => case id; apply Rle_trans with z; auto with real | id : ~ ?x <= ?y, id2 : ~ ?z <= ?x |- _ => case id; apply Rle_trans with z; auto with real end. Qed.