summaryrefslogtreecommitdiff
path: root/theories/Reals/Ranalysis3.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Reals/Ranalysis3.v')
-rw-r--r--theories/Reals/Ranalysis3.v164
1 files changed, 81 insertions, 83 deletions
diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v
index c7d95660..5eaf5a57 100644
--- a/theories/Reals/Ranalysis3.v
+++ b/theories/Reals/Ranalysis3.v
@@ -1,18 +1,16 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Ranalysis3.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import Ranalysis1.
Require Import Ranalysis2.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
(** Division *)
Theorem derivable_pt_lim_div :
@@ -24,17 +22,17 @@ Theorem derivable_pt_lim_div :
Proof.
intros f1 f2 x l1 l2 H H0 H1.
cut (derivable_pt f2 x);
- [ intro X | unfold derivable_pt in |- *; exists l2; exact H0 ].
+ [ intro X | unfold derivable_pt; exists l2; exact H0 ].
assert (H2 := continuous_neq_0 _ _ (derivable_continuous_pt _ _ X) H1).
elim H2; clear H2; intros eps_f2 H2.
- unfold div_fct in |- *.
+ unfold div_fct.
assert (H3 := derivable_continuous_pt _ _ X).
unfold continuity_pt in H3; unfold continue_in in H3; unfold limit1_in in H3;
unfold limit_in in H3; unfold dist in H3.
simpl in H3; unfold R_dist in H3.
elim (H3 (Rabs (f2 x) / 2));
[ idtac
- | unfold Rdiv in |- *; change (0 < Rabs (f2 x) * / 2) in |- *;
+ | unfold Rdiv; change (0 < Rabs (f2 x) * / 2);
apply Rmult_lt_0_compat;
[ apply Rabs_pos_lt; assumption | apply Rinv_0_lt_compat; prove_sup0 ] ].
clear H3; intros alp_f2 H3.
@@ -48,12 +46,12 @@ Proof.
(forall a:R,
Rabs a < Rmin eps_f2 alp_f2 -> / Rabs (f2 (x + a)) < 2 / Rabs (f2 x)).
intro Maj.
- unfold derivable_pt_lim in |- *; intros.
+ unfold derivable_pt_lim; intros.
elim (H (Rabs (eps * f2 x / 8)));
[ idtac
- | unfold Rdiv in |- *; change (0 < Rabs (eps * f2 x * / 8)) in |- *;
+ | unfold Rdiv; change (0 < Rabs (eps * f2 x * / 8));
apply Rabs_pos_lt; repeat apply prod_neq_R0;
- [ red in |- *; intro H7; rewrite H7 in H6; elim (Rlt_irrefl _ H6)
+ [ red; intro H7; rewrite H7 in H6; elim (Rlt_irrefl _ H6)
| assumption
| apply Rinv_neq_0_compat; discrR ] ].
intros alp_f1d H7.
@@ -70,7 +68,7 @@ Proof.
| elim H3; intros; assumption
| apply (cond_pos alp_f1d) ] ].
exists (mkposreal (Rmin eps_f2 (Rmin alp_f2 alp_f1d)) H10).
- simpl in |- *; intros.
+ simpl; intros.
assert (H13 := Rlt_le_trans _ _ _ H12 (Rmin_r _ _)).
assert (H14 := Rlt_le_trans _ _ _ H12 (Rmin_l _ _)).
assert (H15 := Rlt_le_trans _ _ _ H13 (Rmin_r _ _)).
@@ -82,7 +80,7 @@ Proof.
Rabs (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) +
Rabs (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) +
Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x))).
- unfold Rminus in |- *.
+ unfold Rminus.
rewrite <-
(Rabs_Ropp (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) + - f2 x) / h + - l2)))
.
@@ -100,15 +98,15 @@ Proof.
intros.
apply Rlt_4; assumption.
rewrite H8.
- unfold Rdiv in |- *; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
+ unfold Rdiv; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
rewrite Rabs_R0; rewrite Rmult_0_l.
apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup ].
rewrite H8.
- unfold Rdiv in |- *; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
+ unfold Rdiv; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
rewrite Rabs_R0; rewrite Rmult_0_l.
apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup ].
rewrite H9.
- unfold Rdiv in |- *; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
+ unfold Rdiv; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
rewrite Rabs_R0; rewrite Rmult_0_l.
apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup ].
rewrite <- Rabs_mult.
@@ -116,7 +114,7 @@ Proof.
try assumption || apply H2.
apply H14.
apply Rmin_2; assumption.
- right; symmetry in |- *; apply quadruple_var.
+ right; symmetry ; apply quadruple_var.
(***********************************)
(* Second case *)
(* (f1 x)=0 l1<>0 *)
@@ -139,7 +137,7 @@ Proof.
cut (0 < Rmin (Rmin eps_f2 alp_f1d) (Rmin alp_f2 alp_f2t2)).
intro.
exists (mkposreal (Rmin (Rmin eps_f2 alp_f1d) (Rmin alp_f2 alp_f2t2)) H12).
- simpl in |- *.
+ simpl.
intros.
assert (H15 := Rlt_le_trans _ _ _ H14 (Rmin_r _ _)).
assert (H16 := Rlt_le_trans _ _ _ H14 (Rmin_l _ _)).
@@ -154,7 +152,7 @@ Proof.
Rabs (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) +
Rabs (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) +
Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x))).
- unfold Rminus in |- *.
+ unfold Rminus.
rewrite <-
(Rabs_Ropp (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) + - f2 x) / h + - l2)))
.
@@ -172,11 +170,11 @@ Proof.
intros.
apply Rlt_4; assumption.
rewrite H8.
- unfold Rdiv in |- *; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
+ unfold Rdiv; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
rewrite Rabs_R0; rewrite Rmult_0_l.
apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup ].
rewrite H8.
- unfold Rdiv in |- *; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
+ unfold Rdiv; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
rewrite Rabs_R0; rewrite Rmult_0_l.
apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup ].
rewrite <- Rabs_mult.
@@ -187,7 +185,7 @@ Proof.
apply (maj_term1 x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2); try assumption.
apply H2; assumption.
apply Rmin_2; assumption.
- right; symmetry in |- *; apply quadruple_var.
+ right; symmetry ; apply quadruple_var.
apply H2; assumption.
repeat apply Rmin_pos.
apply (cond_pos eps_f2).
@@ -198,21 +196,21 @@ Proof.
elim H10; intros.
case (Req_dec a 0); intro.
rewrite H14; rewrite Rplus_0_r.
- unfold Rminus in |- *; rewrite Rplus_opp_r.
+ unfold Rminus; rewrite Rplus_opp_r.
rewrite Rabs_R0.
apply Rabs_pos_lt.
- unfold Rdiv, Rsqr in |- *; repeat rewrite Rmult_assoc.
+ unfold Rdiv, Rsqr; repeat rewrite Rmult_assoc.
repeat apply prod_neq_R0; try assumption.
- red in |- *; intro; rewrite H15 in H6; elim (Rlt_irrefl _ H6).
+ red; intro; rewrite H15 in H6; elim (Rlt_irrefl _ H6).
apply Rinv_neq_0_compat; repeat apply prod_neq_R0; discrR || assumption.
apply H13.
split.
apply D_x_no_cond; assumption.
replace (x + a - x) with a; [ assumption | ring ].
- change (0 < Rabs (eps * Rsqr (f2 x) / (8 * l1))) in |- *.
- apply Rabs_pos_lt; unfold Rdiv, Rsqr in |- *; repeat rewrite Rmult_assoc;
+ change (0 < Rabs (eps * Rsqr (f2 x) / (8 * l1))).
+ apply Rabs_pos_lt; unfold Rdiv, Rsqr; repeat rewrite Rmult_assoc;
repeat apply prod_neq_R0.
- red in |- *; intro; rewrite H11 in H6; elim (Rlt_irrefl _ H6).
+ red; intro; rewrite H11 in H6; elim (Rlt_irrefl _ H6).
assumption.
assumption.
apply Rinv_neq_0_compat; repeat apply prod_neq_R0;
@@ -225,17 +223,17 @@ Proof.
case (Req_dec l2 0); intro.
elim (H0 (Rabs (Rsqr (f2 x) * eps / (8 * f1 x))));
[ idtac
- | apply Rabs_pos_lt; unfold Rdiv, Rsqr in |- *; repeat rewrite Rmult_assoc;
+ | apply Rabs_pos_lt; unfold Rdiv, Rsqr; repeat rewrite Rmult_assoc;
repeat apply prod_neq_R0;
[ assumption
| assumption
- | red in |- *; intro; rewrite H11 in H6; elim (Rlt_irrefl _ H6)
+ | red; intro; rewrite H11 in H6; elim (Rlt_irrefl _ H6)
| apply Rinv_neq_0_compat; repeat apply prod_neq_R0; discrR || assumption ] ].
intros alp_f2d H12.
cut (0 < Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d alp_f2d)).
intro.
exists (mkposreal (Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d alp_f2d)) H11).
- simpl in |- *.
+ simpl.
intros.
assert (H15 := Rlt_le_trans _ _ _ H14 (Rmin_l _ _)).
assert (H16 := Rlt_le_trans _ _ _ H14 (Rmin_r _ _)).
@@ -250,7 +248,7 @@ Proof.
Rabs (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) +
Rabs (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) +
Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x))).
- unfold Rminus in |- *.
+ unfold Rminus.
rewrite <-
(Rabs_Ropp (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) + - f2 x) / h + - l2)))
.
@@ -268,7 +266,7 @@ Proof.
intros.
apply Rlt_4; assumption.
rewrite H10.
- unfold Rdiv in |- *; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
+ unfold Rdiv; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
rewrite Rabs_R0; rewrite Rmult_0_l.
apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup ].
rewrite <- Rabs_mult.
@@ -276,14 +274,14 @@ Proof.
apply H2; assumption.
apply Rmin_2; assumption.
rewrite H9.
- unfold Rdiv in |- *; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
+ unfold Rdiv; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
rewrite Rabs_R0; rewrite Rmult_0_l.
apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup ].
rewrite <- Rabs_mult.
apply (maj_term1 x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2); assumption || idtac.
apply H2; assumption.
apply Rmin_2; assumption.
- right; symmetry in |- *; apply quadruple_var.
+ right; symmetry ; apply quadruple_var.
apply H2; assumption.
repeat apply Rmin_pos.
apply (cond_pos eps_f2).
@@ -296,7 +294,7 @@ Proof.
(***********************************)
elim (H0 (Rabs (Rsqr (f2 x) * eps / (8 * f1 x))));
[ idtac
- | apply Rabs_pos_lt; unfold Rsqr, Rdiv in |- *;
+ | apply Rabs_pos_lt; unfold Rsqr, Rdiv;
repeat rewrite Rinv_mult_distr; repeat apply prod_neq_R0;
try assumption || discrR ].
intros alp_f2d H11.
@@ -315,7 +313,7 @@ Proof.
exists
(mkposreal (Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d (Rmin alp_f2d alp_f2c)))
H14).
- simpl in |- *; intros.
+ simpl; intros.
assert (H17 := Rlt_le_trans _ _ _ H16 (Rmin_l _ _)).
assert (H18 := Rlt_le_trans _ _ _ H16 (Rmin_r _ _)).
assert (H19 := Rlt_le_trans _ _ _ H18 (Rmin_r _ _)).
@@ -337,7 +335,7 @@ Proof.
Rabs (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) +
Rabs (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) +
Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x))).
- unfold Rminus in |- *.
+ unfold Rminus.
rewrite <-
(Rabs_Ropp (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) + - f2 x) / h + - l2)))
.
@@ -363,24 +361,24 @@ Proof.
apply H2; assumption.
apply Rmin_2; assumption.
rewrite H9.
- unfold Rdiv in |- *; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
+ unfold Rdiv; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
rewrite Rabs_R0; rewrite Rmult_0_l.
apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup ].
rewrite <- Rabs_mult.
apply (maj_term1 x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2); try assumption.
apply H2; assumption.
apply Rmin_2; assumption.
- right; symmetry in |- *; apply quadruple_var.
+ right; symmetry ; apply quadruple_var.
apply H2; assumption.
intros.
case (Req_dec a 0); intro.
rewrite H17; rewrite Rplus_0_r.
- unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0.
+ unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0.
apply Rabs_pos_lt.
- unfold Rdiv, Rsqr in |- *.
+ unfold Rdiv, Rsqr.
repeat rewrite Rinv_mult_distr; try assumption.
repeat apply prod_neq_R0; try assumption.
- red in |- *; intro H18; rewrite H18 in H6; elim (Rlt_irrefl _ H6).
+ red; intro H18; rewrite H18 in H6; elim (Rlt_irrefl _ H6).
apply Rinv_neq_0_compat; discrR.
apply Rinv_neq_0_compat; discrR.
apply Rinv_neq_0_compat; discrR.
@@ -403,19 +401,19 @@ Proof.
apply (cond_pos alp_f1d).
apply (cond_pos alp_f2d).
elim H13; intros; assumption.
- change (0 < Rabs (Rsqr (f2 x) * f2 x * eps / (8 * f1 x * l2))) in |- *.
+ change (0 < Rabs (Rsqr (f2 x) * f2 x * eps / (8 * f1 x * l2))).
apply Rabs_pos_lt.
- unfold Rsqr, Rdiv in |- *.
+ unfold Rsqr, Rdiv.
repeat rewrite Rinv_mult_distr; try assumption || discrR.
repeat apply prod_neq_R0; try assumption.
- red in |- *; intro H13; rewrite H13 in H6; elim (Rlt_irrefl _ H6).
+ red; intro H13; rewrite H13 in H6; elim (Rlt_irrefl _ H6).
apply Rinv_neq_0_compat; discrR.
apply Rinv_neq_0_compat; discrR.
apply Rinv_neq_0_compat; discrR.
apply Rinv_neq_0_compat; assumption.
apply Rinv_neq_0_compat; assumption.
apply prod_neq_R0; [ discrR | assumption ].
- red in |- *; intro H11; rewrite H11 in H6; elim (Rlt_irrefl _ H6).
+ red; intro H11; rewrite H11 in H6; elim (Rlt_irrefl _ H6).
apply Rinv_neq_0_compat; discrR.
apply Rinv_neq_0_compat; discrR.
apply Rinv_neq_0_compat; discrR.
@@ -442,7 +440,7 @@ Proof.
exists
(mkposreal
(Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d (Rmin alp_f2d alp_f2t2))) H13).
- simpl in |- *.
+ simpl.
intros.
cut
(forall a:R,
@@ -464,7 +462,7 @@ Proof.
Rabs (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) +
Rabs (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) +
Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x))).
- unfold Rminus in |- *.
+ unfold Rminus.
rewrite <-
(Rabs_Ropp (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) + - f2 x) / h + - l2)))
.
@@ -482,7 +480,7 @@ Proof.
intros.
apply Rlt_4; assumption.
rewrite H10.
- unfold Rdiv in |- *; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
+ unfold Rdiv; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
rewrite Rabs_R0; rewrite Rmult_0_l.
apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup ].
rewrite <- Rabs_mult.
@@ -497,20 +495,20 @@ Proof.
apply (maj_term1 x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2); try assumption.
apply H2; assumption.
apply Rmin_2; assumption.
- right; symmetry in |- *; apply quadruple_var.
+ right; symmetry ; apply quadruple_var.
apply H2; assumption.
intros.
case (Req_dec a 0); intro.
- rewrite H17; rewrite Rplus_0_r; unfold Rminus in |- *; rewrite Rplus_opp_r;
+ rewrite H17; rewrite Rplus_0_r; unfold Rminus; rewrite Rplus_opp_r;
rewrite Rabs_R0.
apply Rabs_pos_lt.
- unfold Rdiv in |- *; rewrite Rinv_mult_distr; try discrR || assumption.
- unfold Rsqr in |- *.
+ unfold Rdiv; rewrite Rinv_mult_distr; try discrR || assumption.
+ unfold Rsqr.
repeat apply prod_neq_R0;
assumption ||
(apply Rinv_neq_0_compat; assumption) ||
(apply Rinv_neq_0_compat; discrR) ||
- (red in |- *; intro H18; rewrite H18 in H6; elim (Rlt_irrefl _ H6)).
+ (red; intro H18; rewrite H18 in H6; elim (Rlt_irrefl _ H6)).
elim H11; intros.
apply H19.
split.
@@ -523,20 +521,20 @@ Proof.
apply (cond_pos alp_f2d).
elim H11; intros; assumption.
apply Rabs_pos_lt.
- unfold Rdiv, Rsqr in |- *; rewrite Rinv_mult_distr; try discrR || assumption.
+ unfold Rdiv, Rsqr; rewrite Rinv_mult_distr; try discrR || assumption.
repeat apply prod_neq_R0;
assumption ||
(apply Rinv_neq_0_compat; assumption) ||
(apply Rinv_neq_0_compat; discrR) ||
- (red in |- *; intro H12; rewrite H12 in H6; elim (Rlt_irrefl _ H6)).
- change (0 < Rabs (eps * Rsqr (f2 x) / (8 * l1))) in |- *.
+ (red; intro H12; rewrite H12 in H6; elim (Rlt_irrefl _ H6)).
+ change (0 < Rabs (eps * Rsqr (f2 x) / (8 * l1))).
apply Rabs_pos_lt.
- unfold Rdiv, Rsqr in |- *; rewrite Rinv_mult_distr; try discrR || assumption.
+ unfold Rdiv, Rsqr; rewrite Rinv_mult_distr; try discrR || assumption.
repeat apply prod_neq_R0;
assumption ||
(apply Rinv_neq_0_compat; assumption) ||
(apply Rinv_neq_0_compat; discrR) ||
- (red in |- *; intro H12; rewrite H12 in H6; elim (Rlt_irrefl _ H6)).
+ (red; intro H12; rewrite H12 in H6; elim (Rlt_irrefl _ H6)).
(***********************************)
(* Sixth case *)
(* (f1 x)<>0 l1<>0 l2<>0 *)
@@ -564,7 +562,7 @@ Proof.
(mkposreal
(Rmin (Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d alp_f2d))
(Rmin alp_f2c alp_f2t2)) H15).
- simpl in |- *.
+ simpl.
intros.
assert (H18 := Rlt_le_trans _ _ _ H17 (Rmin_l _ _)).
assert (H19 := Rlt_le_trans _ _ _ H17 (Rmin_r _ _)).
@@ -593,7 +591,7 @@ Proof.
Rabs (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) +
Rabs (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) +
Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x))).
- unfold Rminus in |- *.
+ unfold Rminus.
rewrite <-
(Rabs_Ropp (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) + - f2 x) / h + - l2)))
.
@@ -626,18 +624,18 @@ Proof.
apply (maj_term1 x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2); try assumption.
apply H2; assumption.
apply Rmin_2; assumption.
- right; symmetry in |- *; apply quadruple_var.
+ right; symmetry ; apply quadruple_var.
apply H2; assumption.
intros.
case (Req_dec a 0); intro.
- rewrite H18; rewrite Rplus_0_r; unfold Rminus in |- *; rewrite Rplus_opp_r;
+ rewrite H18; rewrite Rplus_0_r; unfold Rminus; rewrite Rplus_opp_r;
rewrite Rabs_R0; apply Rabs_pos_lt.
- unfold Rdiv, Rsqr in |- *; rewrite Rinv_mult_distr.
+ unfold Rdiv, Rsqr; rewrite Rinv_mult_distr.
repeat apply prod_neq_R0;
assumption ||
(apply Rinv_neq_0_compat; assumption) ||
(apply Rinv_neq_0_compat; discrR) ||
- (red in |- *; intro H28; rewrite H28 in H6; elim (Rlt_irrefl _ H6)).
+ (red; intro H28; rewrite H28 in H6; elim (Rlt_irrefl _ H6)).
apply prod_neq_R0; [ discrR | assumption ].
apply prod_neq_R0; [ discrR | assumption ].
assumption.
@@ -648,20 +646,20 @@ Proof.
replace (x + a - x) with a; [ assumption | ring ].
intros.
case (Req_dec a 0); intro.
- rewrite H18; rewrite Rplus_0_r; unfold Rminus in |- *; rewrite Rplus_opp_r;
+ rewrite H18; rewrite Rplus_0_r; unfold Rminus; rewrite Rplus_opp_r;
rewrite Rabs_R0; apply Rabs_pos_lt.
- unfold Rdiv, Rsqr in |- *; rewrite Rinv_mult_distr.
+ unfold Rdiv, Rsqr; rewrite Rinv_mult_distr.
repeat apply prod_neq_R0;
assumption ||
(apply Rinv_neq_0_compat; assumption) ||
(apply Rinv_neq_0_compat; discrR) ||
- (red in |- *; intro H28; rewrite H28 in H6; elim (Rlt_irrefl _ H6)).
+ (red; intro H28; rewrite H28 in H6; elim (Rlt_irrefl _ H6)).
discrR.
assumption.
elim H14; intros.
apply H20.
split.
- unfold D_x, no_cond in |- *; split.
+ unfold D_x, no_cond; split.
trivial.
apply Rminus_not_eq_right.
replace (x + a - x) with a; [ assumption | ring ].
@@ -673,34 +671,34 @@ Proof.
apply (cond_pos alp_f2d).
elim H13; intros; assumption.
elim H14; intros; assumption.
- change (0 < Rabs (eps * Rsqr (f2 x) / (8 * l1))) in |- *; apply Rabs_pos_lt.
- unfold Rdiv, Rsqr in |- *; rewrite Rinv_mult_distr; try discrR || assumption.
+ change (0 < Rabs (eps * Rsqr (f2 x) / (8 * l1))); apply Rabs_pos_lt.
+ unfold Rdiv, Rsqr; rewrite Rinv_mult_distr; try discrR || assumption.
repeat apply prod_neq_R0;
assumption ||
(apply Rinv_neq_0_compat; assumption) ||
(apply Rinv_neq_0_compat; discrR) ||
- (red in |- *; intro H14; rewrite H14 in H6; elim (Rlt_irrefl _ H6)).
- change (0 < Rabs (Rsqr (f2 x) * f2 x * eps / (8 * f1 x * l2))) in |- *;
+ (red; intro H14; rewrite H14 in H6; elim (Rlt_irrefl _ H6)).
+ change (0 < Rabs (Rsqr (f2 x) * f2 x * eps / (8 * f1 x * l2)));
apply Rabs_pos_lt.
- unfold Rdiv, Rsqr in |- *; rewrite Rinv_mult_distr.
+ unfold Rdiv, Rsqr; rewrite Rinv_mult_distr.
repeat apply prod_neq_R0;
assumption ||
(apply Rinv_neq_0_compat; assumption) ||
(apply Rinv_neq_0_compat; discrR) ||
- (red in |- *; intro H13; rewrite H13 in H6; elim (Rlt_irrefl _ H6)).
+ (red; intro H13; rewrite H13 in H6; elim (Rlt_irrefl _ H6)).
apply prod_neq_R0; [ discrR | assumption ].
apply prod_neq_R0; [ discrR | assumption ].
assumption.
apply Rabs_pos_lt.
- unfold Rdiv, Rsqr in |- *; rewrite Rinv_mult_distr;
+ unfold Rdiv, Rsqr; rewrite Rinv_mult_distr;
[ idtac | discrR | assumption ].
repeat apply prod_neq_R0;
assumption ||
(apply Rinv_neq_0_compat; assumption) ||
(apply Rinv_neq_0_compat; discrR) ||
- (red in |- *; intro H11; rewrite H11 in H6; elim (Rlt_irrefl _ H6)).
+ (red; intro H11; rewrite H11 in H6; elim (Rlt_irrefl _ H6)).
intros.
- unfold Rdiv in |- *.
+ unfold Rdiv.
apply Rmult_lt_reg_l with (Rabs (f2 (x + a))).
apply Rabs_pos_lt; apply H2.
apply Rlt_le_trans with (Rmin eps_f2 alp_f2).
@@ -741,13 +739,13 @@ Proof.
unfold Rminus in H7; assumption.
intros.
case (Req_dec x x0); intro.
- rewrite <- H5; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0;
- unfold Rdiv in |- *; apply Rmult_lt_0_compat;
+ rewrite <- H5; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0;
+ unfold Rdiv; apply Rmult_lt_0_compat;
[ apply Rabs_pos_lt; assumption | apply Rinv_0_lt_compat; prove_sup0 ].
elim H3; intros.
apply H7.
split.
- unfold D_x, no_cond in |- *; split.
+ unfold D_x, no_cond; split.
trivial.
assumption.
assumption.
@@ -758,7 +756,7 @@ Lemma derivable_pt_div :
derivable_pt f1 x ->
derivable_pt f2 x -> f2 x <> 0 -> derivable_pt (f1 / f2) x.
Proof.
- unfold derivable_pt in |- *.
+ unfold derivable_pt.
intros f1 f2 x X X0 H.
elim X; intros.
elim X0; intros.
@@ -771,7 +769,7 @@ Lemma derivable_div :
derivable f1 ->
derivable f2 -> (forall x:R, f2 x <> 0) -> derivable (f1 / f2).
Proof.
- unfold derivable in |- *; intros f1 f2 X X0 H x.
+ unfold derivable; intros f1 f2 X X0 H x.
apply (derivable_pt_div _ _ _ (X x) (X0 x) (H x)).
Qed.