diff options
Diffstat (limited to 'theories/Reals/Rpower.v')
| -rw-r--r-- | theories/Reals/Rpower.v | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index c6fac951b..d465523a7 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -25,7 +25,7 @@ Require Import R_sqrt. Require Import Sqrt_reg. Require Import MVT. Require Import Ranalysis4. -Require Import Fourier. +Require Import Lra. Local Open Scope R_scope. Lemma P_Rmin : forall (P:R -> Prop) (x y:R), P x -> P y -> P (Rmin x y). @@ -714,7 +714,7 @@ Qed. Lemma Rlt_Rpower_l a b c: 0 < c -> 0 < a < b -> a ^R c < b ^R c. Proof. intros c0 [a0 ab]; apply exp_increasing. -now apply Rmult_lt_compat_l; auto; apply ln_increasing; fourier. +now apply Rmult_lt_compat_l; auto; apply ln_increasing; lra. Qed. Lemma Rle_Rpower_l a b c: 0 <= c -> 0 < a <= b -> a ^R c <= b ^R c. @@ -722,7 +722,7 @@ Proof. intros [c0 | c0]; [ | intros; rewrite <- c0, !Rpower_O; [apply Rle_refl | |] ]. intros [a0 [ab|ab]]. - now apply Rlt_le, Rlt_Rpower_l;[ | split]; fourier. + now apply Rlt_le, Rlt_Rpower_l;[ | split]; lra. rewrite ab; apply Rle_refl. apply Rlt_le_trans with a; tauto. tauto. @@ -754,10 +754,10 @@ assert (cmp : 0 < x + sqrt (x ^ 2 + 1)). replace (x ^ 2) with ((-x) ^ 2) by ring. assert (sqrt ((- x) ^ 2) < sqrt ((-x)^2+1)). apply sqrt_lt_1_alt. - split;[apply pow_le | ]; fourier. + split;[apply pow_le | ]; lra. pattern x at 1; replace x with (- (sqrt ((- x) ^ 2))). - assert (t:= sqrt_pos ((-x)^2)); fourier. - simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive;[reflexivity | fourier]. + assert (t:= sqrt_pos ((-x)^2)); lra. + simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive;[reflexivity | lra]. apply Rplus_lt_le_0_compat;[apply Rnot_le_gt; assumption | apply sqrt_pos]. rewrite exp_ln;[ | assumption]. rewrite exp_Ropp, exp_ln;[ | assumption]. @@ -770,7 +770,7 @@ apply Rmult_eq_reg_l with (2 * (x + sqrt (x ^ 2 + 1)));[ | apply Rgt_not_eq, Rmult_lt_0_compat;[apply Rlt_0_2 | assumption]]. assert (pow2_sqrt : forall x, 0 <= x -> sqrt x ^ 2 = x) by (intros; simpl; rewrite Rmult_1_r, sqrt_sqrt; auto). -field_simplify;[rewrite pow2_sqrt;[field | ] | apply Rgt_not_eq; fourier]. +field_simplify;[rewrite pow2_sqrt;[field | ] | apply Rgt_not_eq; lra]. apply Rplus_le_le_0_compat;[simpl; rewrite Rmult_1_r; apply (Rle_0_sqr x)|apply Rlt_le, Rlt_0_1]. Qed. @@ -784,12 +784,12 @@ assert (0 < x + sqrt (x ^ 2 + 1)). replace (x ^ 2) with ((-x) ^ 2) by ring. assert (sqrt ((- x) ^ 2) < sqrt ((-x)^2+1)). apply sqrt_lt_1_alt. - split;[apply pow_le|]; fourier. + split;[apply pow_le|]; lra. pattern x at 1; replace x with (- (sqrt ((- x) ^ 2))). - assert (t:= sqrt_pos ((-x)^2)); fourier. - simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive; auto; fourier. + assert (t:= sqrt_pos ((-x)^2)); lra. + simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive; auto; lra. assert (0 < x ^ 2 + 1). - apply Rplus_le_lt_0_compat;[simpl; rewrite Rmult_1_r; apply Rle_0_sqr|fourier]. + apply Rplus_le_lt_0_compat;[simpl; rewrite Rmult_1_r; apply Rle_0_sqr|lra]. replace (/sqrt (x ^ 2 + 1)) with (/(x + sqrt (x ^ 2 + 1)) * (1 + (/(2 * sqrt (x ^ 2 + 1)) * (INR 2 * x ^ 1 + 0)))). @@ -817,7 +817,7 @@ intros x y xy. case (Rle_dec (arcsinh y) (arcsinh x));[ | apply Rnot_le_lt ]. intros abs; case (Rlt_not_le _ _ xy). rewrite <- (sinh_arcsinh y), <- (sinh_arcsinh x). -destruct abs as [lt | q];[| rewrite q; fourier]. +destruct abs as [lt | q];[| rewrite q; lra]. apply Rlt_le, sinh_lt; assumption. Qed. |