diff options
Diffstat (limited to 'theories/Reals/R_sqr.v')
| -rw-r--r-- | theories/Reals/R_sqr.v | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v index 17b6c60d..6460a927 100644 --- a/theories/Reals/R_sqr.v +++ b/theories/Reals/R_sqr.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: R_sqr.v 10710 2008-03-23 09:24:09Z herbelin $ i*) +(*i $Id$ i*) Require Import Rbase. Require Import Rbasic_fun. @@ -61,7 +61,7 @@ Proof. | elim H0; intro; [ elim H; symmetry in |- *; exact H1 | rewrite Rsqr_neg; generalize (Ropp_lt_gt_contravar x 0 H1); - rewrite Ropp_0; intro; unfold Rsqr in |- *; + rewrite Ropp_0; intro; unfold Rsqr in |- *; apply Rmult_lt_0_compat; assumption ] ]. Qed. @@ -103,8 +103,8 @@ Proof. [ assumption | cut (y < x); [ intro; unfold Rsqr in H; - generalize (Rmult_le_0_lt_compat y x y x H1 H1 H2 H2); - intro; generalize (Rle_lt_trans (x * x) (y * y) (x * x) H H3); + generalize (Rmult_le_0_lt_compat y x y x H1 H1 H2 H2); + intro; generalize (Rle_lt_trans (x * x) (y * y) (x * x) H H3); intro; elim (Rlt_irrefl (x * x) H4) | auto with real ] ]. Qed. @@ -115,8 +115,8 @@ Proof. [ assumption | cut (y < x); [ intro; unfold Rsqr in H; - generalize (Rmult_le_0_lt_compat y x y x H0 H0 H1 H1); - intro; generalize (Rle_lt_trans (x * x) (y * y) (x * x) H H2); + generalize (Rmult_le_0_lt_compat y x y x H0 H0 H1 H1); + intro; generalize (Rle_lt_trans (x * x) (y * y) (x * x) H H2); intro; elim (Rlt_irrefl (x * x) H3) | auto with real ] ]. Qed. @@ -152,7 +152,7 @@ Proof. generalize (Ropp_lt_gt_contravar x 0 r); rewrite Ropp_0; intro; generalize (Rlt_le 0 (- x) H1); intro; rewrite (Rsqr_neg x) in H; generalize (Rsqr_incr_0 (- x) y H H2 H0); intro; - rewrite <- (Ropp_involutive x); apply Ropp_ge_le_contravar; + rewrite <- (Ropp_involutive x); apply Ropp_ge_le_contravar; apply Rle_ge; assumption. apply Rle_trans with 0; [ rewrite <- Ropp_0; apply Ropp_ge_le_contravar; apply Rle_ge; assumption @@ -165,7 +165,7 @@ Proof. intros; case (Rcase_abs x); intro. generalize (Ropp_lt_gt_contravar x 0 r); rewrite Ropp_0; intro; generalize (Rlt_le 0 (- x) H2); intro; - generalize (Ropp_le_ge_contravar (- y) x H); rewrite Ropp_involutive; + generalize (Ropp_le_ge_contravar (- y) x H); rewrite Ropp_involutive; intro; generalize (Rge_le y (- x) H4); intro; rewrite (Rsqr_neg x); apply Rsqr_incr_1; assumption. generalize (Rge_le x 0 r); intro; apply Rsqr_incr_1; assumption. @@ -175,9 +175,9 @@ Lemma neg_pos_Rsqr_le : forall x y:R, - y <= x -> x <= y -> Rsqr x <= Rsqr y. Proof. intros; case (Rcase_abs x); intro. generalize (Ropp_lt_gt_contravar x 0 r); rewrite Ropp_0; intro; - generalize (Ropp_le_ge_contravar (- y) x H); rewrite Ropp_involutive; + generalize (Ropp_le_ge_contravar (- y) x H); rewrite Ropp_involutive; intro; generalize (Rge_le y (- x) H2); intro; generalize (Rlt_le 0 (- x) H1); - intro; generalize (Rle_trans 0 (- x) y H4 H3); intro; + intro; generalize (Rle_trans 0 (- x) y H4 H3); intro; rewrite (Rsqr_neg x); apply Rsqr_incr_1; assumption. generalize (Rge_le x 0 r); intro; generalize (Rle_trans 0 x y H1 H0); intro; apply Rsqr_incr_1; assumption. @@ -225,16 +225,16 @@ Proof. intros; unfold Rabs in |- *; case (Rcase_abs x); case (Rcase_abs y); intros. rewrite (Rsqr_neg x) in H; rewrite (Rsqr_neg y) in H; generalize (Ropp_lt_gt_contravar y 0 r); - generalize (Ropp_lt_gt_contravar x 0 r0); rewrite Ropp_0; + generalize (Ropp_lt_gt_contravar x 0 r0); rewrite Ropp_0; intros; generalize (Rlt_le 0 (- x) H0); generalize (Rlt_le 0 (- y) H1); intros; apply Rsqr_inj; assumption. rewrite (Rsqr_neg x) in H; generalize (Rge_le y 0 r); intro; - generalize (Ropp_lt_gt_contravar x 0 r0); rewrite Ropp_0; - intro; generalize (Rlt_le 0 (- x) H1); intro; apply Rsqr_inj; + generalize (Ropp_lt_gt_contravar x 0 r0); rewrite Ropp_0; + intro; generalize (Rlt_le 0 (- x) H1); intro; apply Rsqr_inj; assumption. rewrite (Rsqr_neg y) in H; generalize (Rge_le x 0 r0); intro; - generalize (Ropp_lt_gt_contravar y 0 r); rewrite Ropp_0; - intro; generalize (Rlt_le 0 (- y) H1); intro; apply Rsqr_inj; + generalize (Ropp_lt_gt_contravar y 0 r); rewrite Ropp_0; + intro; generalize (Rlt_le 0 (- y) H1); intro; apply Rsqr_inj; assumption. generalize (Rge_le x 0 r0); generalize (Rge_le y 0 r); intros; apply Rsqr_inj; assumption. |