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. (*******************************)
(*******************************) (*********) 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)intros r1 r2 P H1 H2; unfold Rmin; case (Rle_dec r1 r2); auto. Qed. (*********)forall (r1 r2 : R) (P : R -> Type), P 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) (P : R -> Type), (r1 <= r2 -> P r1) -> (r2 <= r1 -> P r2) -> P (Rmin r1 r2)forall r1 r2 r : R, Rmin r1 r2 > r -> r1 > r /\ r2 > rforall r1 r2 r : R, Rmin r1 r2 > r -> r1 > r /\ r2 > rr1, r2, r:RHle:r1 <= r2H:r1 > rr1 > r /\ r2 > rr1, r2, r:RHnle:~ r1 <= r2H:r2 > rr1 > r /\ r2 > rr1, r2, r:RHle:r1 <= r2H:r1 > rr1 > rr1, r2, r:RHle:r1 <= r2H:r1 > rr2 > rr1, r2, r:RHnle:~ r1 <= r2H:r2 > rr1 > r /\ r2 > rr1, r2, r:RHle:r1 <= r2H:r1 > rr2 > rr1, r2, r:RHnle:~ r1 <= r2H:r2 > rr1 > r /\ r2 > rr1, r2, r:RHnle:~ r1 <= r2H:r2 > rr1 > r /\ r2 > rr1, r2, r:RHnle:~ r1 <= r2H:r2 > rr1 > rr1, r2, r:RHnle:~ r1 <= r2H:r2 > rr2 > rassumption. Qed. (*********)r1, r2, r:RHnle:~ r1 <= r2H:r2 > rr2 > rforall r1 r2 r : R, r1 > r /\ r2 > r -> Rmin r1 r2 > rintros; unfold Rmin; case (Rle_dec r1 r2); elim H; clear H; intros; assumption. Qed. (*********)forall r1 r2 r : R, r1 > r /\ r2 > r -> Rmin r1 r2 > rforall r1 r2 r : R, Rmin r1 r2 > r <-> r1 > r /\ r2 > rforall r1 r2 r : R, Rmin r1 r2 > r <-> r1 > r /\ r2 > rr1, r2, r:RRmin r1 r2 > r -> r1 > r /\ r2 > rr1, r2, r:Rr1 > r /\ r2 > r -> Rmin r1 r2 > rexact (Rmin_Rgt_r r1 r2 r). Qed. (*********)r1, r2, r:Rr1 > r /\ r2 > r -> Rmin r1 r2 > rforall x y : R, Rmin x y <= xintros; unfold Rmin; case (Rle_dec x y); intro H1; [ right; reflexivity | auto with real ]. Qed. (*********)forall x y : R, Rmin x y <= xforall x y : R, Rmin x y <= yintros; unfold Rmin; case (Rle_dec x y); intro H1; [ assumption | auto with real ]. Qed. (*********)forall x y : R, Rmin x y <= yforall x y : R, x <= y -> Rmin x y = xintros; apply Rmin_case_strong; auto using Rle_antisym. Qed. (*********)forall x y : R, x <= y -> Rmin x y = xforall x y : R, y <= x -> Rmin x y = yintros; apply Rmin_case_strong; auto using Rle_antisym. Qed. (*********)forall x y : R, y <= x -> Rmin x y = yforall x y z : R, x <= y -> Rmin x z <= Rmin y zintros; do 2 (apply Rmin_case_strong; intro); eauto using Rle_trans, Rle_refl. Qed. (*********)forall x y z : R, x <= y -> Rmin x z <= Rmin y zforall x y z : R, x <= y -> Rmin z x <= Rmin z yintros; 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 yforall x y : R, Rmin x y = Rmin y xintros; 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 : R, Rmin x y = Rmin y xforall x y : posreal, 0 < Rmin x yintros; apply Rmin_Rgt_r; split; [ apply (cond_pos x) | apply (cond_pos y) ]. Qed. (*********)forall x y : posreal, 0 < Rmin x yforall x y : R, 0 < x -> 0 < y -> 0 < Rmin x yforall x y : R, 0 < x -> 0 < y -> 0 < Rmin x ycase (Rle_dec x y); intro; assumption. Qed. (*********)x, y:RH:0 < xH0:0 < y0 < (if Rle_dec x y then x else y)forall x y z : R, z <= x -> z <= y -> z <= Rmin x yintros; unfold Rmin; case (Rle_dec x y); intro; assumption. Qed. (*********)forall x y z : R, z <= x -> z <= y -> z <= Rmin x yforall x y z : R, z < x -> z < y -> z < Rmin x yintros; unfold Rmin; case (Rle_dec x y); intro; assumption. Qed. (*******************************)forall x y z : R, z < x -> z < y -> z < Rmin x y
(*******************************) (*********) 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)intros r1 r2 P H1 H2; unfold Rmax; case (Rle_dec r1 r2); auto. Qed. (*********)forall (r1 r2 : R) (P : R -> Type), P r1 -> 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) (P : R -> Type), (r2 <= r1 -> P r1) -> (r1 <= r2 -> P r2) -> P (Rmax r1 r2)forall r1 r2 r : R, r <= Rmax r1 r2 <-> r <= r1 \/ r <= r2forall r1 r2 r : R, r <= Rmax r1 r2 <-> r <= r1 \/ r <= r2r1, r2, r:Rr <= Rmax r1 r2 -> r <= r1 \/ r <= r2r1, r2, r:Rr <= r1 \/ r <= r2 -> r <= Rmax r1 r2r1, r2, r:Rr <= r1 \/ r <= r2 -> r <= Rmax r1 r2r1, r2, r:Rr0:r1 <= r2H:r <= r1r <= r2r1, r2, r:RHnle:~ r1 <= r2H:r <= r2r <= r1generalize (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.r1, r2, r:RHnle:~ r1 <= r2H:r <= r2r <= r1forall x y : R, Rmax x y = Rmax y xintros 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, Rmax x y = Rmax y xforall x y : R, x <= Rmax x yintros; unfold Rmax; case (Rle_dec x y); intro H1; [ assumption | auto with real ]. Qed. (*********)forall x y : R, x <= Rmax x yforall x y : R, y <= Rmax x yintros; 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 <= Rmax x yforall x y : R, y <= x -> Rmax x y = xintros; apply Rmax_case_strong; auto using Rle_antisym. Qed. (*********)forall x y : R, y <= x -> Rmax x y = xforall x y : R, x <= y -> Rmax x y = yintros; apply Rmax_case_strong; auto using Rle_antisym. Qed. (*********)forall x y : R, x <= y -> Rmax x y = yforall x y z : R, x <= y -> Rmax x z <= Rmax y zintros; do 2 (apply Rmax_case_strong; intro); eauto using Rle_trans, Rle_refl. Qed. (*********)forall x y z : R, x <= y -> Rmax x z <= Rmax y zforall x y z : R, x <= y -> Rmax z x <= Rmax z yintros; 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 yforall p q r : R, 0 <= r -> Rmax (r * p) (r * q) = r * Rmax p qforall p q r : R, 0 <= r -> Rmax (r * p) (r * q) = r * Rmax p qp, q, r:RH: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:RH:0 <= rH1:~ r * p <= r * qH2:p <= qr * p = r * qp, q, r:RH:0 <= rH1:r * p <= r * qH2:~ p <= qr * q = r * pp, q, r:RH:0 <= rH1:~ r * p <= r * qH2:p <= qE1:0 < rr * p = r * qp, q, r:RH:0 <= rH1:~ r * p <= r * qH2:p <= qE1:0 = rr * p = r * qp, q, r:RH:0 <= rH1:r * p <= r * qH2:~ p <= qr * q = r * pp, q, r:RH:0 <= rH1:~ r * p <= r * qH2:p <= qE1:0 = rr * p = r * qp, q, r:RH:0 <= rH1:r * p <= r * qH2:~ p <= qr * q = r * pp, q, r:RH:0 <= rH1:r * p <= r * qH2:~ p <= qr * q = r * pp, q, r:RH:0 <= rH1:r * p <= r * qH2:~ p <= qE1:0 < rr * q = r * pp, q, r:RH:0 <= rH1:r * p <= r * qH2:~ p <= qE1:0 = rr * q = r * pp, q, r:RH:0 <= rH1:r * p <= r * qH2:~ p <= qE1:0 < rp <= qp, q, r:RH:0 <= rH1:r * p <= r * qH2:~ p <= qE1:0 = rr * q = r * prewrite <- E1; repeat rewrite Rmult_0_l; auto. Qed. (*********)p, q, r:RH:0 <= rH1:r * p <= r * qH2:~ p <= qE1:0 = rr * q = r * pforall x y : negreal, Rmax x y < 0intros; unfold Rmax; case (Rle_dec x y); intro; [ apply (cond_neg y) | apply (cond_neg x) ]. Qed. (*********)forall x y : negreal, Rmax x y < 0forall x y z : R, x <= z -> y <= z -> Rmax x y <= zintros; unfold Rmax; case (Rle_dec x y); intro; assumption. Qed. (*********)forall x y z : R, x <= z -> y <= z -> Rmax x y <= zforall x y z : R, x < z -> y < z -> Rmax x y < zintros; unfold Rmax; case (Rle_dec x y); intro; assumption. Qed.forall x y z : R, x < z -> y < z -> Rmax x y < zforall x y z : R, Rmax x y < z <-> x < z /\ y < zforall x y z : R, Rmax x y < z <-> x < z /\ y < zx, y, z:RRmax x y < z -> x < z /\ y < zx, y, z:Rx < z /\ y < z -> Rmax x y < zx, y, z:Rx <= y -> y < z -> x < z /\ y < zx, y, z:R~ x <= y -> x < z -> x < z /\ y < zx, y, z:Rx < z /\ y < z -> Rmax x y < zx, y, z:R~ x <= y -> x < z -> x < z /\ y < zx, y, z:Rx < z /\ y < z -> Rmax x y < zintros [h h']; apply Rmax_lub_lt; assumption. Qed. (*********)x, y, z:Rx < z /\ y < z -> Rmax x y < zforall x y : R, x < 0 -> y < 0 -> Rmax x y < 0forall x y : R, x < 0 -> y < 0 -> Rmax x y < 0case (Rle_dec x y); intro; assumption. Qed. (*******************************)x, y:RH:x < 0H0:y < 0(if Rle_dec x y then y else x) < 0
(*******************************) (*********)forall r : R, {r < 0} + {r >= 0}forall r : R, {r < 0} + {r >= 0}r:RH:0 <= r{r < 0} + {r >= 0}r:RH:~ 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. (*********)r:RH:~ 0 <= r{r < 0} + {r >= 0}Rabs 0 = 0Rabs 0 = 0generalize (Rlt_irrefl 0); intro; exfalso; auto. Qed.r:0 < 0- 0 = 0Rabs 1 = 1Rabs 1 = 1intros H; absurd (1 < 0); auto with real. Qed. (*********)1 < 0 -> - (1) = 1forall r : R, r <> 0 -> Rabs r <> 0forall r : R, r <> 0 -> Rabs r <> 0apply Ropp_neq_0_compat; auto. Qed. (*********)r:RH:r <> 0r0:r < 0- r <> 0forall r : R, r < 0 -> Rabs r = - rforall r : R, r < 0 -> Rabs r = - rr:RH:r < 0r0:r >= 0~ r >= 0r:RH:r < 0r0:r >= 0r >= 0assumption. Qed. (*********)r:RH:r < 0r0:r >= 0r >= 0forall r : R, r >= 0 -> Rabs r = rforall r : R, r >= 0 -> Rabs r = rr:RH:r >= 0Hlt:r < 0- r = rr:RH, Hge:r >= 0r = rr:RH:r >= 0Hlt:r < 0~ r >= 0r:RH:r >= 0Hlt:r < 0r >= 0r:RH, Hge:r >= 0r = rr:RH:r >= 0Hlt:r < 0r >= 0r:RH, Hge:r >= 0r = rtrivial. Qed.r:RH, Hge:r >= 0r = rforall a : R, a <= 0 -> Rabs a = - aforall a : R, a <= 0 -> Rabs a = - aa:RH:a <= 0H1:a < 0Rabs a = - aa:RH:a <= 0H1:a = 0Rabs a = - arewrite H1; simpl; rewrite Rabs_right; auto with real. Qed. (*********)a:RH:a <= 0H1:a = 0Rabs a = - aforall x : R, 0 <= Rabs xforall x : R, 0 <= Rabs xx:RHlt:x < 00 <= - xx:RHge:x >= 00 <= xapply Rge_le; assumption. Qed.x:RHge:x >= 00 <= xforall x : R, x <= Rabs xforall x : R, x <= Rabs xapply Rminus_le; rewrite <- Rplus_0_r; unfold Rminus; rewrite Ropp_involutive; auto with real. Qed. Definition RRle_abs := Rle_abs.x:Rr:x < 0x <= - xforall a b : R, - b <= a <= b -> Rabs a <= bforall a b : R, - b <= a <= b -> Rabs a <= ba, b:Ra < 0 -> - b <= a <= b -> - a <= ba, b:Ra >= 0 -> - b <= a <= b -> a <= bintros _ [_ it]; exact it. Qed. (*********)a, b:Ra >= 0 -> - b <= a <= b -> a <= bforall x : R, 0 <= x -> Rabs x = xintros; unfold Rabs; case (Rcase_abs x) as [Hlt|Hge]; [ generalize (Rgt_not_le 0 x Hlt); intro; exfalso; auto | trivial ]. Qed. (*********)forall x : R, 0 <= x -> Rabs x = xforall x : R, Rabs (Rabs x) = Rabs xintro; apply (Rabs_pos_eq (Rabs x) (Rabs_pos x)). Qed. (*********)forall x : R, Rabs (Rabs x) = Rabs xforall x : R, x <> 0 -> 0 < Rabs xforall x : R, x <> 0 -> 0 < Rabs xapply Rabs_no_R0 in H; symmetry in Heq; contradiction. Qed. (*********)x:RH:x <> 0Heq:0 = Rabs x0 < Rabs xforall x y : R, Rabs (x - y) = Rabs (y - x)forall x y : R, Rabs (x - y) = Rabs (y - x)x, y:RHlt:x - y < 0Hlt':y - x < 0- (x - y) = - (y - x)x, y:RHlt:x - y < 0Hge':y - x >= 0- (x - y) = y - xx, y:RHge:x - y >= 0Hlt':y - x < 0x - y = - (y - x)x, y:RHge:x - y >= 0Hge':y - x >= 0x - y = y - xx, y:RHlt:x - y < 0Hge':y - x >= 0- (x - y) = y - xx, y:RHge:x - y >= 0Hlt':y - x < 0x - y = - (y - x)x, y:RHge:x - y >= 0Hge':y - x >= 0x - y = y - xx, y:RHge:x - y >= 0Hlt':y - x < 0x - y = - (y - x)x, y:RHge:x - y >= 0Hge':y - x >= 0x - y = y - xx, y:RHge:x - y >= 0Hge':y - x >= 0x - y = y - xx, y:RH:x - y > 0H0:y - x > 0x - y = y - xx, y:RH:x - y > 0H0:y - x = 0x - y = y - xx, y:RH:x - y = 0H0:y - x > 0x - y = y - xx, y:RH:x - y = 0H0:y - x = 0x - y = y - xx, y:RH:x - y > 0H0:y - x = 0x - y = y - xx, y:RH:x - y = 0H0:y - x > 0x - y = y - xx, y:RH:x - y = 0H0:y - x = 0x - y = y - xx, y:RH:x - y = 0H0:y - x > 0x - y = y - xx, y:RH:x - y = 0H0:y - x = 0x - y = y - xapply Rminus_diag_uniq in H0 as ->; trivial. Qed. (*********)x, y:RH:x - y = 0H0:y - x = 0x - y = y - xforall x y : R, Rabs (x * y) = Rabs x * Rabs yforall x y : R, Rabs (x * y) = Rabs x * Rabs yx, y:RHlt:x * y < 0Hltx:x < 0Hlty:y < 0- (x * y) = - x * - yx, y:RHlt:x * y < 0Hltx:x < 0Hgey:y >= 0- (x * y) = - x * yx, y:RHlt:x * y < 0Hgex:x >= 0Hlty:y < 0- (x * y) = x * - yx, y:RHlt:x * y < 0Hgex:x >= 0Hgey:y >= 0- (x * y) = x * yx, y:RHge:x * y >= 0Hltx:x < 0Hlty:y < 0x * y = - x * - yx, y:RHge:x * y >= 0Hltx:x < 0Hgey:y >= 0x * y = - x * yx, y:RHge:x * y >= 0Hgex:x >= 0Hlty:y < 0x * y = x * - yx, y:RHlt:x * y < 0Hltx:x < 0Hlty:~ x * y < x * 0- (x * y) = - x * - yx, y:RHlt:x * y < 0Hltx:x < 0Hgey:y >= 0- (x * y) = - x * yx, y:RHlt:x * y < 0Hgex:x >= 0Hlty:y < 0- (x * y) = x * - yx, y:RHlt:x * y < 0Hgex:x >= 0Hgey:y >= 0- (x * y) = x * yx, y:RHge:x * y >= 0Hltx:x < 0Hlty:y < 0x * y = - x * - yx, y:RHge:x * y >= 0Hltx:x < 0Hgey:y >= 0x * y = - x * yx, y:RHge:x * y >= 0Hgex:x >= 0Hlty:y < 0x * y = x * - yx, y:RHlt:x * y < 0Hltx:x < 0Hgey:y >= 0- (x * y) = - x * yx, y:RHlt:x * y < 0Hgex:x >= 0Hlty:y < 0- (x * y) = x * - yx, y:RHlt:x * y < 0Hgex:x >= 0Hgey:y >= 0- (x * y) = x * yx, y:RHge:x * y >= 0Hltx:x < 0Hlty:y < 0x * y = - x * - yx, y:RHge:x * y >= 0Hltx:x < 0Hgey:y >= 0x * y = - x * yx, y:RHge:x * y >= 0Hgex:x >= 0Hlty:y < 0x * y = x * - yx, y:RHlt:x * y < 0Hgex:x >= 0Hlty:y < 0- (x * y) = x * - yx, y:RHlt:x * y < 0Hgex:x >= 0Hgey:y >= 0- (x * y) = x * yx, y:RHge:x * y >= 0Hltx:x < 0Hlty:y < 0x * y = - x * - yx, y:RHge:x * y >= 0Hltx:x < 0Hgey:y >= 0x * y = - x * yx, y:RHge:x * y >= 0Hgex:x >= 0Hlty:y < 0x * y = x * - yx, y:RHlt:x * y < 0Hgex:x >= 0Hgey:y >= 0- (x * y) = x * yx, y:RHge:x * y >= 0Hltx:x < 0Hlty:y < 0x * y = - x * - yx, y:RHge:x * y >= 0Hltx:x < 0Hgey:y >= 0x * y = - x * yx, y:RHge:x * y >= 0Hgex:x >= 0Hlty:y < 0x * y = x * - yx, y:RHlt:x * y < 0H:x > 0H0:y > 0- (x * y) = x * yx:RHlt:x * 0 < 0H:x > 0- (x * 0) = x * 0y:RHlt:0 * y < 0H:y > 0- (0 * y) = 0 * yHlt:0 * 0 < 0- (0 * 0) = 0 * 0x, y:RHge:x * y >= 0Hltx:x < 0Hlty:y < 0x * y = - x * - yx, y:RHge:x * y >= 0Hltx:x < 0Hgey:y >= 0x * y = - x * yx, y:RHge:x * y >= 0Hgex:x >= 0Hlty:y < 0x * y = x * - yx, y:RHlt:x * y < 0H:x > 0H0:~ x * y < x * 0- (x * y) = x * yx:RHlt:x * 0 < 0H:x > 0- (x * 0) = x * 0y:RHlt:0 * y < 0H:y > 0- (0 * y) = 0 * yHlt:0 * 0 < 0- (0 * 0) = 0 * 0x, y:RHge:x * y >= 0Hltx:x < 0Hlty:y < 0x * y = - x * - yx, y:RHge:x * y >= 0Hltx:x < 0Hgey:y >= 0x * y = - x * yx, y:RHge:x * y >= 0Hgex:x >= 0Hlty:y < 0x * y = x * - yx:RHlt:x * 0 < 0H:x > 0- (x * 0) = x * 0y:RHlt:0 * y < 0H:y > 0- (0 * y) = 0 * yHlt:0 * 0 < 0- (0 * 0) = 0 * 0x, y:RHge:x * y >= 0Hltx:x < 0Hlty:y < 0x * y = - x * - yx, y:RHge:x * y >= 0Hltx:x < 0Hgey:y >= 0x * y = - x * yx, y:RHge:x * y >= 0Hgex:x >= 0Hlty:y < 0x * y = x * - yy:RHlt:0 * y < 0H:y > 0- (0 * y) = 0 * yHlt:0 * 0 < 0- (0 * 0) = 0 * 0x, y:RHge:x * y >= 0Hltx:x < 0Hlty:y < 0x * y = - x * - yx, y:RHge:x * y >= 0Hltx:x < 0Hgey:y >= 0x * y = - x * yx, y:RHge:x * y >= 0Hgex:x >= 0Hlty:y < 0x * y = x * - yHlt:0 * 0 < 0- (0 * 0) = 0 * 0x, y:RHge:x * y >= 0Hltx:x < 0Hlty:y < 0x * y = - x * - yx, y:RHge:x * y >= 0Hltx:x < 0Hgey:y >= 0x * y = - x * yx, y:RHge:x * y >= 0Hgex:x >= 0Hlty:y < 0x * y = x * - yx, y:RHge:x * y >= 0Hltx:x < 0Hlty:y < 0x * y = - x * - yx, y:RHge:x * y >= 0Hltx:x < 0Hgey:y >= 0x * y = - x * yx, y:RHge:x * y >= 0Hgex:x >= 0Hlty:y < 0x * y = x * - yx, y:RHge:x * y >= 0Hltx:x < 0Hgey:y >= 0x * y = - x * yx, y:RHge:x * y >= 0Hgex:x >= 0Hlty:y < 0x * y = x * - yx, y:RH:x * y > 0Hltx:x < 0Hgey:y >= 0x * y = - x * yx, y:RH:x * y = 0Hltx:x < 0Hgey:y >= 0x * y = - x * yx, y:RHge:x * y >= 0Hgex:x >= 0Hlty:y < 0x * y = x * - yx, y:RH:x * y > 0Hltx:x < 0H0:y > 0x * y = - x * yx, y:RH:x * y > 0Hltx:x < 0H0:y = 0x * y = - x * yx, y:RH:x * y = 0Hltx:x < 0Hgey:y >= 0x * y = - x * yx, y:RHge:x * y >= 0Hgex:x >= 0Hlty:y < 0x * y = x * - yx, y:RH:x * y > 0Hltx:~ 0 * y < x * yH0:y > 0x * y = - x * yx, y:RH:x * y > 0Hltx:x < 0H0:y = 0x * y = - x * yx, y:RH:x * y = 0Hltx:x < 0Hgey:y >= 0x * y = - x * yx, y:RHge:x * y >= 0Hgex:x >= 0Hlty:y < 0x * y = x * - yx, y:RH:x * y > 0Hltx:x < 0H0:y = 0x * y = - x * yx, y:RH:x * y = 0Hltx:x < 0Hgey:y >= 0x * y = - x * yx, y:RHge:x * y >= 0Hgex:x >= 0Hlty:y < 0x * y = x * - yx, y:RH:x * y = 0Hltx:x < 0Hgey:y >= 0x * y = - x * yx, y:RHge:x * y >= 0Hgex:x >= 0Hlty:y < 0x * y = x * - yx, y:RHge:x * y >= 0Hgex:x >= 0Hlty:y < 0x * y = x * - yx, y:RH:x * y > 0Hgex:x >= 0Hlty:y < 0x * y = x * - yx, y:RH:x * y = 0Hgex:x >= 0Hlty:y < 0x * y = x * - yx, y:RH:x * y > 0H0:x > 0Hlty:y < 0x * y = x * - yx, y:RH:x * y > 0H0:x = 0Hlty:y < 0x * y = x * - yx, y:RH:x * y = 0Hgex:x >= 0Hlty:y < 0x * y = x * - yx, y:RH:x * y > 0H0:x > 0Hlty:~ x * 0 < x * yx * y = x * - yx, y:RH:x * y > 0H0:x = 0Hlty:y < 0x * y = x * - yx, y:RH:x * y = 0Hgex:x >= 0Hlty:y < 0x * y = x * - yx, y:RH:x * y > 0H0:x = 0Hlty:y < 0x * y = x * - yx, y:RH:x * y = 0Hgex:x >= 0Hlty:y < 0x * y = x * - yrewrite <- Ropp_mult_distr_r, H, Ropp_0; trivial. Qed. (*********)x, y:RH:x * y = 0Hgex:x >= 0Hlty:y < 0x * y = x * - yforall r : R, r <> 0 -> Rabs (/ r) = / Rabs rforall r : R, r <> 0 -> Rabs (/ r) = / Rabs rr:RHlt:r < 0Hlt':/ r < 0H:r <> 0- / r = / - rr:RHlt:r < 0Hge':/ r >= 0H:r <> 0/ r = / - rr:RHge:r >= 0Hlt':/ r < 0H:r <> 0- / r = / rr:RHlt:r < 0Hge':/ r >= 0H:r <> 0/ r = / - rr:RHge:r >= 0Hlt':/ r < 0H:r <> 0- / r = / rr:RHlt:r < 0Hge':/ r >= 0H:r <> 0/ r = - / rr:RHge:r >= 0Hlt':/ r < 0H:r <> 0- / r = / rr:RHlt:r < 0H0:/ r > 0H:r <> 0/ r = - / rr:RHlt:r < 0H:r <> 00 = - 0r:RHge:r >= 0Hlt':/ r < 0H:r <> 0- / r = / rr:RHlt:r < 0H:r <> 00 = - 0r:RHge:r >= 0Hlt':/ r < 0H:r <> 0- / r = / rr:RHge:r >= 0Hlt':/ r < 0H:r <> 0- / r = / rr:RH0:r > 0Hlt':/ r < 0H:r <> 0- / r = / rH:0 <> 0Hlt':/ 0 < 0- / 0 = / 0contradiction (refl_equal 0). Qed.H:0 <> 0Hlt':/ 0 < 0- / 0 = / 0forall x : R, Rabs (- x) = Rabs xforall x : R, Rabs (- x) = Rabs xx:RRabs (-1 * x) = Rabs xx:RRabs (-1) * Rabs x = Rabs xx:R1 * Rabs x = Rabs xx:R1 = Rabs (-1)x:R1 = Rabs (-1)x:R-1 < 0 -> 1 = - -1x:R-1 >= 0 -> 1 = -1x:R-1 >= 0 -> 1 = -1x:R-1 >= - 0 -> 1 = -1x:RH0:0 >= IPR 11 = -1apply Rlt_0_1. Qed. (*********)x:RH0:0 >= IPR 10 < IPR 1forall a b : R, Rabs (a + b) <= Rabs a + Rabs bforall a b : R, Rabs (a + b) <= Rabs a + Rabs ba, b:RHlt:a + b < 0Hlta:a < 0Hltb:b < 0- (a + b) <= - a + - ba, b:RHlt:a + b < 0Hlta:a < 0Hgeb:b >= 0- (a + b) <= - a + ba, b:RHlt:a + b < 0Hgea:a >= 0Hltb:b < 0- (a + b) <= a + - ba, b:RHlt:a + b < 0Hgea:a >= 0Hgeb:b >= 0- (a + b) <= a + ba, b:RHge:a + b >= 0Hlta:a < 0Hltb:b < 0a + b <= - a + - ba, b:RHge:a + b >= 0Hlta:a < 0Hgeb:b >= 0a + b <= - a + ba, b:RHge:a + b >= 0Hgea:a >= 0Hltb:b < 0a + b <= a + - ba, b:RHge:a + b >= 0Hgea:a >= 0Hgeb:b >= 0a + b <= a + b(**)a, b:RHlt:a + b < 0Hlta:a < 0Hgeb:b >= 0- (a + b) <= - a + ba, b:RHlt:a + b < 0Hgea:a >= 0Hltb:b < 0- (a + b) <= a + - ba, b:RHlt:a + b < 0Hgea:a >= 0Hgeb:b >= 0- (a + b) <= a + ba, b:RHge:a + b >= 0Hlta:a < 0Hltb:b < 0a + b <= - a + - ba, b:RHge:a + b >= 0Hlta:a < 0Hgeb:b >= 0a + b <= - a + ba, b:RHge:a + b >= 0Hgea:a >= 0Hltb:b < 0a + b <= a + - ba, b:RHge:a + b >= 0Hgea:a >= 0Hgeb:b >= 0a + b <= a + ba, b:RHlt:a + b < 0Hlta:a < 0Hgeb:b >= 0H:b > 0- b < b \/ - b = ba, b:RHlt:a + b < 0Hlta:a < 0Hgeb:b >= 0H:b = 0- b < b \/ - b = ba, b:RHlt:a + b < 0Hgea:a >= 0Hltb:b < 0- (a + b) <= a + - ba, b:RHlt:a + b < 0Hgea:a >= 0Hgeb:b >= 0- (a + b) <= a + ba, b:RHge:a + b >= 0Hlta:a < 0Hltb:b < 0a + b <= - a + - ba, b:RHge:a + b >= 0Hlta:a < 0Hgeb:b >= 0a + b <= - a + ba, b:RHge:a + b >= 0Hgea:a >= 0Hltb:b < 0a + b <= a + - ba, b:RHge:a + b >= 0Hgea:a >= 0Hgeb:b >= 0a + b <= a + ba, b:RHlt:a + b < 0Hlta:a < 0Hgeb:b >= 0H:b = 0- b < b \/ - b = ba, b:RHlt:a + b < 0Hgea:a >= 0Hltb:b < 0- (a + b) <= a + - ba, b:RHlt:a + b < 0Hgea:a >= 0Hgeb:b >= 0- (a + b) <= a + ba, b:RHge:a + b >= 0Hlta:a < 0Hltb:b < 0a + b <= - a + - ba, b:RHge:a + b >= 0Hlta:a < 0Hgeb:b >= 0a + b <= - a + ba, b:RHge:a + b >= 0Hgea:a >= 0Hltb:b < 0a + b <= a + - ba, b:RHge:a + b >= 0Hgea:a >= 0Hgeb:b >= 0a + b <= a + b(**)a, b:RHlt:a + b < 0Hgea:a >= 0Hltb:b < 0- (a + b) <= a + - ba, b:RHlt:a + b < 0Hgea:a >= 0Hgeb:b >= 0- (a + b) <= a + ba, b:RHge:a + b >= 0Hlta:a < 0Hltb:b < 0a + b <= - a + - ba, b:RHge:a + b >= 0Hlta:a < 0Hgeb:b >= 0a + b <= - a + ba, b:RHge:a + b >= 0Hgea:a >= 0Hltb:b < 0a + b <= a + - ba, b:RHge:a + b >= 0Hgea:a >= 0Hgeb:b >= 0a + b <= a + ba, b:RHlt:a + b < 0Hgea:a >= 0Hltb:b < 0H:a > 0- a < a \/ - a = aa, b:RHlt:a + b < 0Hgea:a >= 0Hltb:b < 0H:a = 0- a < a \/ - a = aa, b:RHlt:a + b < 0Hgea:a >= 0Hgeb:b >= 0- (a + b) <= a + ba, b:RHge:a + b >= 0Hlta:a < 0Hltb:b < 0a + b <= - a + - ba, b:RHge:a + b >= 0Hlta:a < 0Hgeb:b >= 0a + b <= - a + ba, b:RHge:a + b >= 0Hgea:a >= 0Hltb:b < 0a + b <= a + - ba, b:RHge:a + b >= 0Hgea:a >= 0Hgeb:b >= 0a + b <= a + ba, b:RHlt:a + b < 0Hgea:a >= 0Hltb:b < 0H:a = 0- a < a \/ - a = aa, b:RHlt:a + b < 0Hgea:a >= 0Hgeb:b >= 0- (a + b) <= a + ba, b:RHge:a + b >= 0Hlta:a < 0Hltb:b < 0a + b <= - a + - ba, b:RHge:a + b >= 0Hlta:a < 0Hgeb:b >= 0a + b <= - a + ba, b:RHge:a + b >= 0Hgea:a >= 0Hltb:b < 0a + b <= a + - ba, b:RHge:a + b >= 0Hgea:a >= 0Hgeb:b >= 0a + b <= a + b(**)a, b:RHlt:a + b < 0Hgea:a >= 0Hgeb:b >= 0- (a + b) <= a + ba, b:RHge:a + b >= 0Hlta:a < 0Hltb:b < 0a + b <= - a + - ba, b:RHge:a + b >= 0Hlta:a < 0Hgeb:b >= 0a + b <= - a + ba, b:RHge:a + b >= 0Hgea:a >= 0Hltb:b < 0a + b <= a + - ba, b:RHge:a + b >= 0Hgea:a >= 0Hgeb:b >= 0a + b <= a + ba, b:RHlt:a + b < 0Hgea:a >= 0Hgeb:b >= 0H:a + b > 0Falsea, b:RHlt:a + b < 0Hgea:a >= 0Hgeb:b >= 0H:a + b = 0Falsea, b:RHge:a + b >= 0Hlta:a < 0Hltb:b < 0a + b <= - a + - ba, b:RHge:a + b >= 0Hlta:a < 0Hgeb:b >= 0a + b <= - a + ba, b:RHge:a + b >= 0Hgea:a >= 0Hltb:b < 0a + b <= a + - ba, b:RHge:a + b >= 0Hgea:a >= 0Hgeb:b >= 0a + b <= a + ba, b:RHlt:a + b < 0Hgea:a >= 0Hgeb:b >= 0H:a + b = 0Falsea, b:RHge:a + b >= 0Hlta:a < 0Hltb:b < 0a + b <= - a + - ba, b:RHge:a + b >= 0Hlta:a < 0Hgeb:b >= 0a + b <= - a + ba, b:RHge:a + b >= 0Hgea:a >= 0Hltb:b < 0a + b <= a + - ba, b:RHge:a + b >= 0Hgea:a >= 0Hgeb:b >= 0a + b <= a + ba, b:RHlt:a + b < 0Hgea:a >= 0Hgeb:b >= 0H:a + b = 0a + b <> 0a, b:RHge:a + b >= 0Hlta:a < 0Hltb:b < 0a + b <= - a + - ba, b:RHge:a + b >= 0Hlta:a < 0Hgeb:b >= 0a + b <= - a + ba, b:RHge:a + b >= 0Hgea:a >= 0Hltb:b < 0a + b <= a + - ba, b:RHge:a + b >= 0Hgea:a >= 0Hgeb:b >= 0a + b <= a + b(**)a, b:RHge:a + b >= 0Hlta:a < 0Hltb:b < 0a + b <= - a + - ba, b:RHge:a + b >= 0Hlta:a < 0Hgeb:b >= 0a + b <= - a + ba, b:RHge:a + b >= 0Hgea:a >= 0Hltb:b < 0a + b <= a + - ba, b:RHge:a + b >= 0Hgea:a >= 0Hgeb:b >= 0a + b <= a + ba, b:RH:a + b > 0Hlta:a < 0Hltb:b < 0H0:a + b < 0Falsea, b:RH:a + b = 0Hlta:a < 0Hltb:b < 0H0:a + b < 0Falsea, b:RHge:a + b >= 0Hlta:a < 0Hgeb:b >= 0a + b <= - a + ba, b:RHge:a + b >= 0Hgea:a >= 0Hltb:b < 0a + b <= a + - ba, b:RHge:a + b >= 0Hgea:a >= 0Hgeb:b >= 0a + b <= a + ba, b:RH:a + b = 0Hlta:a < 0Hltb:b < 0H0:a + b < 0Falsea, b:RHge:a + b >= 0Hlta:a < 0Hgeb:b >= 0a + b <= - a + ba, b:RHge:a + b >= 0Hgea:a >= 0Hltb:b < 0a + b <= a + - ba, b:RHge:a + b >= 0Hgea:a >= 0Hgeb:b >= 0a + b <= a + b(**)a, b:RHge:a + b >= 0Hlta:a < 0Hgeb:b >= 0a + b <= - a + ba, b:RHge:a + b >= 0Hgea:a >= 0Hltb:b < 0a + b <= a + - ba, b:RHge:a + b >= 0Hgea:a >= 0Hgeb:b >= 0a + b <= a + b(**)a, b:RHge:a + b >= 0Hgea:a >= 0Hltb:b < 0a + b <= a + - ba, b:RHge:a + b >= 0Hgea:a >= 0Hgeb:b >= 0a + b <= a + b(**) unfold Rle; right; reflexivity. Qed. (*********)a, b:RHge:a + b >= 0Hgea:a >= 0Hgeb:b >= 0a + b <= a + bforall a b : R, Rabs a - Rabs b <= Rabs (a - b)forall a b : R, Rabs a - Rabs b <= Rabs (a - b)a, b:RRabs (a + 0) <= Rabs b + Rabs (a + - b)a, b:RRabs (a + 0) = Rabs aa, b:RRabs (b + (a + - b)) <= Rabs b + Rabs (a + - b)a, b:RRabs (a + 0) = Rabs arewrite (proj1 (Rplus_ne a)); trivial. Qed. (* ||a|-|b||<=|a-b| *)a, b:RRabs (a + 0) = Rabs aforall 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:RHlt:Rabs a < Rabs bRabs (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:RHeq:Rabs a = Rabs bRabs (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:RHgt:Rabs a > Rabs bRabs (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:RHlt:Rabs a < Rabs bRabs (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:RHeq:Rabs a = Rabs bRabs (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:RHgt:Rabs a > Rabs bRabs (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:RHeq:Rabs a = Rabs bRabs (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:RHgt:Rabs a > Rabs bRabs (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:RHgt:Rabs a > Rabs bRabs (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:RH:Rabs b <= Rabs aRabs a - Rabs b <= Rabs (a - b)a, b:RH:Rabs b <= Rabs aRabs 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. (*********)a, b:RH:Rabs b <= Rabs aRabs a - Rabs b = Rabs (Rabs a - Rabs b)forall x a : R, x < a -> - a < x -> Rabs x < aforall x a : R, x < a -> - a < x -> Rabs x < ax, a:RH:x < aH0:- a < xr:x < 0- x < ax, a:RH:x < aH0:- a < xr:x >= 0x < aassumption. Qed. (*********)x, a:RH:x < aH0:- a < xr:x >= 0x < aforall x a : R, Rabs x < a -> x < a /\ - a < xforall x a : R, Rabs x < a -> x < a /\ - a < xx:RHlt:x < 0a:RH:- x < ax < a /\ - a < xx:RHge:x >= 0a:RH:x < ax < a /\ - a < xx:RHlt:x < 0a:RH:- x < aH0:0 < - xH1:0 < ax < ax:RHlt:x < 0a:RH:- x < aH0:0 < - xH1:0 < a- a < xx:RHge:x >= 0a:RH:x < ax < a /\ - a < xx:RHlt:x < 0a:RH:- x < aH0:0 < - xH1:0 < a- a < xx:RHge:x >= 0a:RH:x < ax < a /\ - a < xfold (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.x:RHge:x >= 0a:RH:x < ax < a /\ - a < xforall 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:RH':p <= qH'0:q <= rH'1:0 <= pRabs q <= Rmax (Rabs p) (Rabs r)p, q, r:RH':p <= qH'0:q <= rH'1:p < 0Rabs q <= Rmax (Rabs p) (Rabs r)p, q, r:RH':p <= qH'0:q <= rH'1:0 <= pq <= Rmax p rp, q, r:RH':p <= qH'0:q <= rH'1:0 <= pr >= 0p, q, r:RH':p <= qH'0:q <= rH'1:0 <= pq >= 0p, q, r:RH':p <= qH'0:q <= rH'1:p < 0Rabs q <= Rmax (Rabs p) (Rabs r)p, q, r:RH':p <= qH'0:q <= rH'1:0 <= pr <= Rmax p rp, q, r:RH':p <= qH'0:q <= rH'1:0 <= pr >= 0p, q, r:RH':p <= qH'0:q <= rH'1:0 <= pq >= 0p, q, r:RH':p <= qH'0:q <= rH'1:p < 0Rabs q <= Rmax (Rabs p) (Rabs r)p, q, r:RH':p <= qH'0:q <= rH'1:0 <= pr >= 0p, q, r:RH':p <= qH'0:q <= rH'1:0 <= pq >= 0p, q, r:RH':p <= qH'0:q <= rH'1:p < 0Rabs q <= Rmax (Rabs p) (Rabs r)p, q, r:RH':p <= qH'0:q <= rH'1:0 <= pq >= 0p, q, r:RH':p <= qH'0:q <= rH'1:p < 0Rabs q <= Rmax (Rabs p) (Rabs r)p, q, r:RH':p <= qH'0:q <= rH'1:p < 0Rabs q <= Rmax (Rabs p) (Rabs r)p, q, r:RH':p <= qH'0:q <= rH'1:p < 0Rabs q <= Rmax (- p) (Rabs r)p, q, r:RH':p <= qH'0:q <= rH'1:p < 0H'2:0 <= qRabs q <= Rmax (- p) (Rabs r)p, q, r:RH':p <= qH'0:q <= rH'1:p < 0H'2:q < 0Rabs q <= Rmax (- p) (Rabs r)p, q, r:RH':p <= qH'0:q <= rH'1:p < 0H'2:0 <= qq <= Rmax (- p) rp, q, r:RH':p <= qH'0:q <= rH'1:p < 0H'2:0 <= qr >= 0p, q, r:RH':p <= qH'0:q <= rH'1:p < 0H'2:q < 0Rabs q <= Rmax (- p) (Rabs r)p, q, r:RH':p <= qH'0:q <= rH'1:p < 0H'2:0 <= qr <= Rmax (- p) rp, q, r:RH':p <= qH'0:q <= rH'1:p < 0H'2:0 <= qr >= 0p, q, r:RH':p <= qH'0:q <= rH'1:p < 0H'2:q < 0Rabs q <= Rmax (- p) (Rabs r)p, q, r:RH':p <= qH'0:q <= rH'1:p < 0H'2:0 <= qr >= 0p, q, r:RH':p <= qH'0:q <= rH'1:p < 0H'2:q < 0Rabs q <= Rmax (- p) (Rabs r)p, q, r:RH':p <= qH'0:q <= rH'1:p < 0H'2:q < 0Rabs q <= Rmax (- p) (Rabs r)p, q, r:RH':p <= qH'0:q <= rH'1:p < 0H'2:q < 0- q <= Rmax (- p) (Rabs r)p, q, r:RH':p <= qH'0:q <= rH'1:p < 0H'2:q < 0H'3:0 <= r- q <= Rmax (- p) (Rabs r)p, q, r:RH':p <= qH'0:q <= rH'1:p < 0H'2:q < 0H'3:r < 0- q <= Rmax (- p) (Rabs r)p, q, r:RH':p <= qH'0:q <= rH'1:p < 0H'2:q < 0H'3:0 <= r- q <= Rmax (- p) rp, q, r:RH':p <= qH'0:q <= rH'1:p < 0H'2:q < 0H'3:r < 0- q <= Rmax (- p) (Rabs r)p, q, r:RH':p <= qH'0:q <= rH'1:p < 0H'2:q < 0H'3:0 <= r- p <= Rmax (- p) rp, q, r:RH':p <= qH'0:q <= rH'1:p < 0H'2:q < 0H'3:r < 0- q <= Rmax (- p) (Rabs r)p, q, r:RH':p <= qH'0:q <= rH'1:p < 0H'2:q < 0H'3:r < 0- q <= Rmax (- p) (Rabs r)p, q, r:RH':p <= qH'0:q <= rH'1:p < 0H'2:q < 0H'3:r < 0- q <= Rmax (- p) (- r)apply RmaxLess1; auto. Qed.p, q, r:RH':p <= qH'0:q <= rH'1:p < 0H'2:q < 0H'3:r < 0- p <= Rmax (- p) (- r)forall z : Z, Rabs (IZR z) = IZR (Z.abs z)forall z : Z, Rabs (IZR z) = IZR (Z.abs z)z:ZRabs 0 = 0z:Zforall p : positive, Rabs (IZR (Z.pos p)) = IZR (Z.pos p)z:Zforall p : positive, Rabs (IZR (Z.neg p)) = IZR (Z.pos p)z:Zforall p : positive, Rabs (IZR (Z.pos p)) = IZR (Z.pos p)z:Zforall p : positive, Rabs (IZR (Z.neg p)) = IZR (Z.pos p)z:Zforall p : positive, Rabs (IZR (Z.neg p)) = IZR (Z.pos p)z:Zforall p : positive, Rabs (- IPR p) = IZR (Z.pos p)now apply Rabs_pos_eq, (IZR_le 0). Qed.z:Zp0:positiveRabs (IPR p0) = IZR (Z.pos p0)forall z : Z, IZR (Z.abs z) = Rabs (IZR z)forall z : Z, IZR (Z.abs z) = Rabs (IZR z)now rewrite Rabs_Zabs. Qed.z:ZIZR (Z.abs z) = Rabs (IZR z)forall x y : R, - Rmax x y = Rmin (- x) (- y)x, y:Ry <= x -> - x = Rmin (- x) (- y)x, y:Rx <= y -> - y = Rmin (- x) (- y)now intros w; rewrite Rmin_right; [ | apply Rge_le, Ropp_le_ge_contravar]. Qed.x, y:Rx <= y -> - y = Rmin (- x) (- y)forall x y : R, - Rmin x y = Rmax (- x) (- y)x, y:Rx <= y -> - x = Rmax (- x) (- y)x, y:Ry <= x -> - y = Rmax (- x) (- y)now intros w; rewrite Rmax_right; [ | apply Rge_le, Ropp_le_ge_contravar]. Qed.x, y:Ry <= x -> - y = Rmax (- x) (- y)forall a b c : R, Rmax a (Rmax b c) = Rmax (Rmax a b) cforall a b c : R, Rmax a (Rmax b c) = Rmax (Rmax a b) cunfold 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.a, b, c:RRmax a (Rmax b c) = Rmax (Rmax a b) cforall a b : R, Rmin a b <= Rmax a bforall a b : R, Rmin a b <= Rmax a ba, b:Rr:a <= bRmin a b <= Rmax a ba, b:Rn:~ a <= bRmin a b <= Rmax a bnow rewrite Rmin_right, Rmax_left; assumption || apply Rlt_le, Rnot_le_gt. Qed.a, b:Rn:~ a <= bRmin a b <= Rmax a bforall x y z : R, Rmin x (Rmin y z) = Rmin (Rmin x y) zforall x y z : R, Rmin x (Rmin y z) = Rmin (Rmin x y) zunfold 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.a, b, c:RRmin a (Rmin b c) = Rmin (Rmin a b) c