diff options
| -rw-r--r-- | theories/Reals/Ranalysis4.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v index b2287efc2..52cfb2a7a 100644 --- a/theories/Reals/Ranalysis4.v +++ b/theories/Reals/Ranalysis4.v @@ -19,6 +19,7 @@ Require Ranalysis1. Require R_sqrt. Require Ranalysis2. Require Ranalysis3. +Require Export Exp_prop. Require Export Rtrigo_reg. Require Export Sqrt_reg. @@ -237,8 +238,6 @@ Intros; Unfold derivable; Intro; Apply derivable_pt_finite_sum. Qed. (* Regularity of hyperbolic functions *) -Axiom derivable_pt_lim_exp : (x:R) (derivable_pt_lim exp x (exp x)). - Lemma derivable_pt_lim_cosh : (x:R) (derivable_pt_lim cosh x ``(sinh x)``). Intro. Unfold cosh sinh; Unfold Rdiv. |