diff options
author | Yves Bertot <bertot@inria.fr> | 2014-09-23 13:11:24 +0200 |
---|---|---|
committer | Yves Bertot <bertot@inria.fr> | 2014-09-23 13:11:24 +0200 |
commit | 13ab2df9ed3a5ea6b7455ea8a7da4341e7f2bcd5 (patch) | |
tree | fd42f041d099700403dfc0a3af69ea5791ec5930 /theories/Reals/Ranalysis4.v | |
parent | 85355cfda7a01fa532f111ee7c4d522a8be8a399 (diff) |
adds general facts in the Reals library, whose need was detected in
experiments about computing PI
Diffstat (limited to 'theories/Reals/Ranalysis4.v')
-rw-r--r-- | theories/Reals/Ranalysis4.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v index dd8e0dd52..2f097c4ae 100644 --- a/theories/Reals/Ranalysis4.v +++ b/theories/Reals/Ranalysis4.v @@ -13,6 +13,7 @@ Require Import Rtrigo1. Require Import Ranalysis1. Require Import Ranalysis3. Require Import Exp_prop. +Require Import MVT. Local Open Scope R_scope. (**********) @@ -398,3 +399,14 @@ Proof. intro; apply derive_pt_eq_0. apply derivable_pt_lim_sinh. Qed. + +Lemma sinh_lt : forall x y, x < y -> sinh x < sinh y. +intros x y xy; destruct (MVT_cor2 sinh cosh x y xy) as [c [Pc _]]. + intros; apply derivable_pt_lim_sinh. +apply Rplus_lt_reg_l with (Ropp (sinh x)); rewrite Rplus_opp_l, Rplus_comm. +unfold Rminus at 1 in Pc; rewrite Pc; apply Rmult_lt_0_compat;[ | ]. + unfold cosh; apply Rmult_lt_0_compat;[|apply Rinv_0_lt_compat, Rlt_0_2]. + now apply Rplus_lt_0_compat; apply exp_pos. +now apply Rlt_Rminus; assumption. +Qed. + |