diff options
Diffstat (limited to 'theories/Reals/Ranalysis4.v')
| -rw-r--r-- | theories/Reals/Ranalysis4.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v index 86f49cd4..40bb2429 100644 --- a/theories/Reals/Ranalysis4.v +++ b/theories/Reals/Ranalysis4.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Ranalysis4.v,v 1.19.2.1 2004/07/16 19:31:12 herbelin Exp $ i*) +(*i $Id: Ranalysis4.v 8670 2006-03-28 22:16:14Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -20,13 +20,13 @@ Require Import Exp_prop. Open Local Scope R_scope. Lemma derivable_pt_inv : forall (f:R -> R) (x:R), f x <> 0 -> derivable_pt f x -> derivable_pt (/ f) x. -intros; cut (derivable_pt (fct_cte 1 / f) x -> derivable_pt (/ f) x). -intro; apply X0. +intros f x H X; cut (derivable_pt (fct_cte 1 / f) x -> derivable_pt (/ f) x). +intro X0; apply X0. apply derivable_pt_div. apply derivable_pt_const. assumption. assumption. -unfold div_fct, inv_fct, fct_cte in |- *; intro; elim X0; intros; +unfold div_fct, inv_fct, fct_cte in |- *; intro X0; elim X0; intros; unfold derivable_pt in |- *; apply existT with x0; unfold derivable_pt_abs in |- *; unfold derivable_pt_lim in |- *; unfold derivable_pt_abs in p; unfold derivable_pt_lim in p; @@ -76,8 +76,8 @@ Qed. (**********) Lemma derivable_inv : forall f:R -> R, (forall x:R, f x <> 0) -> derivable f -> derivable (/ f). -intros. -unfold derivable in |- *; intro. +intros f H X. +unfold derivable in |- *; intro x. apply derivable_pt_inv. apply (H x). apply (X x). @@ -381,4 +381,4 @@ Lemma derive_pt_sinh : forall x:R, derive_pt sinh x (derivable_pt_sinh x) = cosh x. intro; apply derive_pt_eq_0. apply derivable_pt_lim_sinh. -Qed.
\ No newline at end of file +Qed. |