diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-07-18 17:21:01 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-07-18 17:21:01 +0200 |
| commit | 8271b23dd0a26bba79c7d6dadd92d2329945675c (patch) | |
| tree | 6d6b4faeda0fc272c1faaa7912406097ef055caa /theories/Reals/R_sqrt.v | |
| parent | e5e3725fab9daa810a4c8a383886f1c5dc980e85 (diff) | |
| parent | 8c43e795c772090b336c0f170a6e5dcab196125d (diff) | |
Merge PR #7897: Remove fourier plugin
Diffstat (limited to 'theories/Reals/R_sqrt.v')
| -rw-r--r-- | theories/Reals/R_sqrt.v | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index d4035fad6..6991923b1 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -155,6 +155,22 @@ Proof. | apply (sqrt_positivity x (Rlt_le 0 x H1)) ]. Qed. +Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y. +intros x y H H0; try assumption. +replace 0 with (x * 0). +apply Rmult_lt_compat_l; auto with real. +ring. +Qed. + +Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y. +intros x y H H0; try assumption. +case H; intros. +red; left. +apply Rlt_mult_inv_pos; auto with real. +rewrite <- H1. +red; right; ring. +Qed. + Lemma sqrt_div_alt : forall x y : R, 0 < y -> sqrt (x / y) = sqrt x / sqrt y. Proof. @@ -176,14 +192,14 @@ Proof. clearbody Hx'. clear Hx. apply Rsqr_inj. apply sqrt_pos. - apply Fourier_util.Rle_mult_inv_pos. + apply Rle_mult_inv_pos. apply Rsqrt_positivity. now apply sqrt_lt_R0. rewrite Rsqr_div, 2!Rsqr_sqrt. unfold Rsqr. now rewrite Rsqrt_Rsqrt. now apply Rlt_le. - now apply Fourier_util.Rle_mult_inv_pos. + now apply Rle_mult_inv_pos. apply Rgt_not_eq. now apply sqrt_lt_R0. Qed. |