Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 413 insertions, 265 deletions

diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v
index 70f7adb1f..a02c5da6c 100644
--- a/theories/Reals/Ranalysis2.v
+++ b/theories/Reals/Ranalysis2.v
@@ -8,295 +8,443 @@
 
 (*i $Id$ i*)
 
-Require Rbase.
-Require Rfunctions.
-Require Ranalysis1.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+Require Import Rbase.
+Require Import Rfunctions.
+Require Import Ranalysis1. Open Local Scope R_scope.
 
 (**********)
-Lemma formule : (x,h,l1,l2:R;f1,f2:R->R) ``h<>0`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ``((f1 (x+h))/(f2 (x+h))-(f1 x)/(f2 x))/h-(l1*(f2 x)-l2*(f1 x))/(Rsqr (f2 x))`` == ``/(f2 (x+h))*(((f1 (x+h))-(f1 x))/h-l1) + l1/((f2 x)*(f2 (x+h)))*((f2 x)-(f2 (x+h))) - (f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))-(f2 x))/h-l2) + (l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))*((f2 (x+h))-(f2 x))``.
-Intros; Unfold Rdiv Rminus Rsqr.
-Repeat Rewrite Rmult_Rplus_distrl; Repeat Rewrite Rmult_Rplus_distr; Repeat Rewrite Rinv_Rmult; Try Assumption.
-Replace ``l1*(f2 x)*(/(f2 x)*/(f2 x))`` with ``l1*/(f2 x)*((f2 x)*/(f2 x))``; [Idtac | Ring].
-Replace ``l1*(/(f2 x)*/(f2 (x+h)))*(f2 x)`` with ``l1*/(f2 (x+h))*((f2 x)*/(f2 x))``; [Idtac | Ring].
-Replace ``l1*(/(f2 x)*/(f2 (x+h)))* -(f2 (x+h))`` with ``-(l1*/(f2 x)*((f2 (x+h))*/(f2 (x+h))))``; [Idtac | Ring].
-Replace ``(f1 x)*(/(f2 x)*/(f2 (x+h)))*((f2 (x+h))*/h)`` with ``(f1 x)*/(f2 x)*/h*((f2 (x+h))*/(f2 (x+h)))``; [Idtac | Ring].
-Replace ``(f1 x)*(/(f2 x)*/(f2 (x+h)))*( -(f2 x)*/h)`` with ``-((f1 x)*/(f2 (x+h))*/h*((f2 x)*/(f2 x)))``; [Idtac | Ring].
-Replace ``(l2*(f1 x)*(/(f2 x)*/(f2 x)*/(f2 (x+h)))*(f2 (x+h)))`` with ``l2*(f1 x)*/(f2 x)*/(f2 x)*((f2 (x+h))*/(f2 (x+h)))``; [Idtac | Ring].
-Replace ``l2*(f1 x)*(/(f2 x)*/(f2 x)*/(f2 (x+h)))* -(f2 x)`` with ``-(l2*(f1 x)*/(f2 x)*/(f2 (x+h))*((f2 x)*/(f2 x)))``; [Idtac | Ring].
-Repeat Rewrite <- Rinv_r_sym; Try Assumption Orelse Ring.
-Apply prod_neq_R0; Assumption.
+Lemma formule :
+ forall (x h l1 l2:R) (f1 f2:R -> R),
+   h <> 0 ->
+   f2 x <> 0 ->
+   f2 (x + h) <> 0 ->
+   (f1 (x + h) / f2 (x + h) - f1 x / f2 x) / h -
+   (l1 * f2 x - l2 * f1 x) / Rsqr (f2 x) =
+   / f2 (x + h) * ((f1 (x + h) - f1 x) / h - l1) +
+   l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h)) -
+   f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2) +
+   l2 * f1 x / (Rsqr (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x).
+intros; unfold Rdiv, Rminus, Rsqr in |- *.
+repeat rewrite Rmult_plus_distr_r; repeat rewrite Rmult_plus_distr_l;
+ repeat rewrite Rinv_mult_distr; try assumption.
+replace (l1 * f2 x * (/ f2 x * / f2 x)) with (l1 * / f2 x * (f2 x * / f2 x));
+ [ idtac | ring ].
+replace (l1 * (/ f2 x * / f2 (x + h)) * f2 x) with
+ (l1 * / f2 (x + h) * (f2 x * / f2 x)); [ idtac | ring ].
+replace (l1 * (/ f2 x * / f2 (x + h)) * - f2 (x + h)) with
+ (- (l1 * / f2 x * (f2 (x + h) * / f2 (x + h)))); [ idtac | ring ].
+replace (f1 x * (/ f2 x * / f2 (x + h)) * (f2 (x + h) * / h)) with
+ (f1 x * / f2 x * / h * (f2 (x + h) * / f2 (x + h))); 
+ [ idtac | ring ].
+replace (f1 x * (/ f2 x * / f2 (x + h)) * (- f2 x * / h)) with
+ (- (f1 x * / f2 (x + h) * / h * (f2 x * / f2 x))); 
+ [ idtac | ring ].
+replace (l2 * f1 x * (/ f2 x * / f2 x * / f2 (x + h)) * f2 (x + h)) with
+ (l2 * f1 x * / f2 x * / f2 x * (f2 (x + h) * / f2 (x + h)));
+ [ idtac | ring ].
+replace (l2 * f1 x * (/ f2 x * / f2 x * / f2 (x + h)) * - f2 x) with
+ (- (l2 * f1 x * / f2 x * / f2 (x + h) * (f2 x * / f2 x))); 
+ [ idtac | ring ].
+repeat rewrite <- Rinv_r_sym; try assumption || ring.
+apply prod_neq_R0; assumption.
 Qed.
 
-Lemma Rmin_pos : (x,y:R) ``0<x`` -> ``0<y`` -> ``0 < (Rmin x y)``.
-Intros; Unfold Rmin.
-Case (total_order_Rle x y); Intro; Assumption.
+Lemma Rmin_pos : forall x y:R, 0 < x -> 0 < y -> 0 < Rmin x y.
+intros; unfold Rmin in |- *.
+case (Rle_dec x y); intro; assumption.
 Qed.
 
-Lemma maj_term1 : (x,h,eps,l1,alp_f2:R;eps_f2,alp_f1d:posreal;f1,f2:R->R) ``0 < eps`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ((h:R)``h <> 0``->``(Rabsolu h) < alp_f1d``->``(Rabsolu (((f1 (x+h))-(f1 x))/h-l1)) < (Rabsolu ((eps*(f2 x))/8))``) -> ((a:R)``(Rabsolu a) < (Rmin eps_f2 alp_f2)``->``/(Rabsolu (f2 (x+a))) < 2/(Rabsolu (f2 x))``) -> ``h<>0`` -> ``(Rabsolu h)<alp_f1d`` -> ``(Rabsolu h) < (Rmin eps_f2 alp_f2)`` -> ``(Rabsolu (/(f2 (x+h))*(((f1 (x+h))-(f1 x))/h-l1))) < eps/4``.
-Intros.
-Assert H7 := (H3 h H6).
-Assert H8 := (H2 h H4 H5).
-Apply Rle_lt_trans with ``2/(Rabsolu (f2 x))*(Rabsolu (((f1 (x+h))-(f1 x))/h-l1))``.
-Rewrite Rabsolu_mult.
-Apply Rle_monotony_r.
-Apply Rabsolu_pos.
-Rewrite Rabsolu_Rinv; [Left; Exact H7 | Assumption].
-Apply Rlt_le_trans with ``2/(Rabsolu (f2 x))*(Rabsolu ((eps*(f2 x))/8))``.
-Apply Rlt_monotony.
-Unfold Rdiv; Apply Rmult_lt_pos; [Sup0 | Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Assumption].
-Exact H8.
-Right; Unfold Rdiv.
-Repeat Rewrite Rabsolu_mult.
-Rewrite Rabsolu_Rinv; DiscrR.
-Replace ``(Rabsolu 8)`` with ``8``.
-Replace ``8`` with ``2*4``; [Idtac | Ring].
-Rewrite Rinv_Rmult; [Idtac | DiscrR | DiscrR].
-Replace ``2*/(Rabsolu (f2 x))*((Rabsolu eps)*(Rabsolu (f2 x))*(/2*/4))`` with ``(Rabsolu eps)*/4*(2*/2)*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))``; [Idtac | Ring].
-Replace (Rabsolu eps) with eps.
-Repeat Rewrite <- Rinv_r_sym; Try DiscrR Orelse (Apply Rabsolu_no_R0; Assumption).
-Ring.
-Symmetry; Apply Rabsolu_right; Left; Assumption.
-Symmetry; Apply Rabsolu_right; Left; Sup.
+Lemma maj_term1 :
+ forall (x h eps l1 alp_f2:R) (eps_f2 alp_f1d:posreal) 
+   (f1 f2:R -> R),
+   0 < eps ->
+   f2 x <> 0 ->
+   f2 (x + h) <> 0 ->
+   (forall h:R,
+      h <> 0 ->
+      Rabs h < alp_f1d ->
+      Rabs ((f1 (x + h) - f1 x) / h - l1) < Rabs (eps * f2 x / 8)) ->
+   (forall a:R,
+      Rabs a < Rmin eps_f2 alp_f2 -> / Rabs (f2 (x + a)) < 2 / Rabs (f2 x)) ->
+   h <> 0 ->
+   Rabs h < alp_f1d ->
+   Rabs h < Rmin eps_f2 alp_f2 ->
+   Rabs (/ f2 (x + h) * ((f1 (x + h) - f1 x) / h - l1)) < eps / 4.
+intros.
+assert (H7 := H3 h H6).
+assert (H8 := H2 h H4 H5).
+apply Rle_lt_trans with
+ (2 / Rabs (f2 x) * Rabs ((f1 (x + h) - f1 x) / h - l1)).
+rewrite Rabs_mult.
+apply Rmult_le_compat_r.
+apply Rabs_pos.
+rewrite Rabs_Rinv; [ left; exact H7 | assumption ].
+apply Rlt_le_trans with (2 / Rabs (f2 x) * Rabs (eps * f2 x / 8)).
+apply Rmult_lt_compat_l.
+unfold Rdiv in |- *; apply Rmult_lt_0_compat;
+ [ prove_sup0 | apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption ].
+exact H8.
+right; unfold Rdiv in |- *.
+repeat rewrite Rabs_mult.
+rewrite Rabs_Rinv; discrR.
+replace (Rabs 8) with 8.
+replace 8 with 8; [ idtac | ring ].
+rewrite Rinv_mult_distr; [ idtac | discrR | discrR ].
+replace (2 * / Rabs (f2 x) * (Rabs eps * Rabs (f2 x) * (/ 2 * / 4))) with
+ (Rabs eps * / 4 * (2 * / 2) * (Rabs (f2 x) * / Rabs (f2 x)));
+ [ idtac | ring ].
+replace (Rabs eps) with eps.
+repeat rewrite <- Rinv_r_sym; try discrR || (apply Rabs_no_R0; assumption).
+ring.
+symmetry  in |- *; apply Rabs_right; left; assumption.
+symmetry  in |- *; apply Rabs_right; left; prove_sup.
 Qed.
 
-Lemma maj_term2 : (x,h,eps,l1,alp_f2,alp_f2t2:R;eps_f2:posreal;f2:R->R) ``0 < eps`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ((a:R)``(Rabsolu a) < alp_f2t2``->``(Rabsolu ((f2 (x+a))-(f2 x))) < (Rabsolu ((eps*(Rsqr (f2 x)))/(8*l1)))``)-> ((a:R)``(Rabsolu a) < (Rmin eps_f2 alp_f2)``->``/(Rabsolu (f2 (x+a))) < 2/(Rabsolu (f2 x))``) -> ``h<>0`` -> ``(Rabsolu h)<alp_f2t2`` -> ``(Rabsolu h) < (Rmin eps_f2 alp_f2)`` -> ``l1<>0`` -> ``(Rabsolu (l1/((f2 x)*(f2 (x+h)))*((f2 x)-(f2 (x+h))))) < eps/4``.
-Intros.
-Assert H8 := (H3 h H6).
-Assert H9 := (H2 h H5).
-Apply Rle_lt_trans with ``(Rabsolu (l1/((f2 x)*(f2 (x+h)))))*(Rabsolu ((eps*(Rsqr (f2 x)))/(8*l1)))``.
-Rewrite Rabsolu_mult; Apply Rle_monotony.
-Apply Rabsolu_pos.
-Rewrite <- (Rabsolu_Ropp ``(f2 x)-(f2 (x+h))``); Rewrite Ropp_distr2.
-Left; Apply H9.
-Apply Rlt_le_trans with ``(Rabsolu (2*l1/((f2 x)*(f2 x))))*(Rabsolu ((eps*(Rsqr (f2 x)))/(8*l1)))``.
-Apply Rlt_monotony_r.
-Apply Rabsolu_pos_lt.
-Unfold Rdiv; Unfold Rsqr; Repeat Apply prod_neq_R0; Try Assumption Orelse DiscrR.
-Red; Intro H10; Rewrite H10 in H; Elim (Rlt_antirefl ? H).
-Apply Rinv_neq_R0; Apply prod_neq_R0; Try Assumption Orelse DiscrR.
-Unfold Rdiv.
-Repeat Rewrite Rinv_Rmult; Try Assumption.
-Repeat Rewrite Rabsolu_mult.
-Replace ``(Rabsolu 2)`` with ``2``.
-Rewrite (Rmult_sym ``2``).
-Replace ``(Rabsolu l1)*((Rabsolu (/(f2 x)))*(Rabsolu (/(f2 x))))*2`` with ``(Rabsolu l1)*((Rabsolu (/(f2 x)))*((Rabsolu (/(f2 x)))*2))``; [Idtac | Ring].
-Repeat Apply Rlt_monotony.
-Apply Rabsolu_pos_lt; Assumption.
-Apply Rabsolu_pos_lt; Apply Rinv_neq_R0; Assumption.
-Repeat Rewrite Rabsolu_Rinv; Try Assumption.
-Rewrite <- (Rmult_sym ``2``).
-Unfold Rdiv in H8; Exact H8.
-Symmetry; Apply Rabsolu_right; Left; Sup0.
-Right.
-Unfold Rsqr Rdiv.
-Do 1 Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR.
-Do 1 Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR.
-Repeat Rewrite Rabsolu_mult.
-Repeat Rewrite Rabsolu_Rinv; Try Assumption Orelse DiscrR.
-Replace (Rabsolu eps) with eps.
-Replace ``(Rabsolu (8))`` with ``8``.
-Replace ``(Rabsolu 2)`` with ``2``.
-Replace ``8`` with ``4*2``; [Idtac | Ring].
-Rewrite Rinv_Rmult; DiscrR.
-Replace ``2*((Rabsolu l1)*(/(Rabsolu (f2 x))*/(Rabsolu (f2 x))))*(eps*((Rabsolu (f2 x))*(Rabsolu (f2 x)))*(/4*/2*/(Rabsolu l1)))`` with ``eps*/4*((Rabsolu l1)*/(Rabsolu l1))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*(2*/2)``; [Idtac | Ring].
-Repeat Rewrite <- Rinv_r_sym; Try (Apply Rabsolu_no_R0; Assumption) Orelse DiscrR.
-Ring.
-Symmetry; Apply Rabsolu_right; Left; Sup0.
-Symmetry; Apply Rabsolu_right; Left; Sup.
-Symmetry; Apply Rabsolu_right; Left; Assumption.
+Lemma maj_term2 :
+ forall (x h eps l1 alp_f2 alp_f2t2:R) (eps_f2:posreal) 
+   (f2:R -> R),
+   0 < eps ->
+   f2 x <> 0 ->
+   f2 (x + h) <> 0 ->
+   (forall a:R,
+      Rabs a < alp_f2t2 ->
+      Rabs (f2 (x + a) - f2 x) < Rabs (eps * Rsqr (f2 x) / (8 * l1))) ->
+   (forall a:R,
+      Rabs a < Rmin eps_f2 alp_f2 -> / Rabs (f2 (x + a)) < 2 / Rabs (f2 x)) ->
+   h <> 0 ->
+   Rabs h < alp_f2t2 ->
+   Rabs h < Rmin eps_f2 alp_f2 ->
+   l1 <> 0 -> Rabs (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) < eps / 4.
+intros.
+assert (H8 := H3 h H6).
+assert (H9 := H2 h H5).
+apply Rle_lt_trans with
+ (Rabs (l1 / (f2 x * f2 (x + h))) * Rabs (eps * Rsqr (f2 x) / (8 * l1))).
+rewrite Rabs_mult; apply Rmult_le_compat_l.
+apply Rabs_pos.
+rewrite <- (Rabs_Ropp (f2 x - f2 (x + h))); rewrite Ropp_minus_distr.
+left; apply H9.
+apply Rlt_le_trans with
+ (Rabs (2 * (l1 / (f2 x * f2 x))) * Rabs (eps * Rsqr (f2 x) / (8 * l1))).
+apply Rmult_lt_compat_r.
+apply Rabs_pos_lt.
+unfold Rdiv in |- *; unfold Rsqr in |- *; repeat apply prod_neq_R0;
+ try assumption || discrR.
+red in |- *; intro H10; rewrite H10 in H; elim (Rlt_irrefl _ H).
+apply Rinv_neq_0_compat; apply prod_neq_R0; try assumption || discrR.
+unfold Rdiv in |- *.
+repeat rewrite Rinv_mult_distr; try assumption.
+repeat rewrite Rabs_mult.
+replace (Rabs 2) with 2.
+rewrite (Rmult_comm 2).
+replace (Rabs l1 * (Rabs (/ f2 x) * Rabs (/ f2 x)) * 2) with
+ (Rabs l1 * (Rabs (/ f2 x) * (Rabs (/ f2 x) * 2))); 
+ [ idtac | ring ].
+repeat apply Rmult_lt_compat_l.
+apply Rabs_pos_lt; assumption.
+apply Rabs_pos_lt; apply Rinv_neq_0_compat; assumption.
+repeat rewrite Rabs_Rinv; try assumption.
+rewrite <- (Rmult_comm 2).
+unfold Rdiv in H8; exact H8.
+symmetry  in |- *; apply Rabs_right; left; prove_sup0.
+right.
+unfold Rsqr, Rdiv in |- *.
+do 1 rewrite Rinv_mult_distr; try assumption || discrR.
+do 1 rewrite Rinv_mult_distr; try assumption || discrR.
+repeat rewrite Rabs_mult.
+repeat rewrite Rabs_Rinv; try assumption || discrR.
+replace (Rabs eps) with eps.
+replace (Rabs 8) with 8.
+replace (Rabs 2) with 2.
+replace 8 with (4 * 2); [ idtac | ring ].
+rewrite Rinv_mult_distr; discrR.
+replace
+ (2 * (Rabs l1 * (/ Rabs (f2 x) * / Rabs (f2 x))) *
+  (eps * (Rabs (f2 x) * Rabs (f2 x)) * (/ 4 * / 2 * / Rabs l1))) with
+ (eps * / 4 * (Rabs l1 * / Rabs l1) * (Rabs (f2 x) * / Rabs (f2 x)) *
+  (Rabs (f2 x) * / Rabs (f2 x)) * (2 * / 2)); [ idtac | ring ].
+repeat rewrite <- Rinv_r_sym; try (apply Rabs_no_R0; assumption) || discrR.
+ring.
+symmetry  in |- *; apply Rabs_right; left; prove_sup0.
+symmetry  in |- *; apply Rabs_right; left; prove_sup.
+symmetry  in |- *; apply Rabs_right; left; assumption.
 Qed.
 
-Lemma maj_term3 : (x,h,eps,l2,alp_f2:R;eps_f2,alp_f2d:posreal;f1,f2:R->R) ``0 < eps`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ((h:R)``h <> 0``->``(Rabsolu h) < alp_f2d``->``(Rabsolu (((f2 (x+h))-(f2 x))/h-l2)) < (Rabsolu (((Rsqr (f2 x))*eps)/(8*(f1 x))))``) -> ((a:R)``(Rabsolu a) < (Rmin eps_f2 alp_f2)``->``/(Rabsolu (f2 (x+a))) < 2/(Rabsolu (f2 x))``) -> ``h<>0`` -> ``(Rabsolu h)<alp_f2d`` -> ``(Rabsolu h) < (Rmin eps_f2 alp_f2)`` -> ``(f1 x)<>0`` -> ``(Rabsolu ((f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))-(f2 x))/h-l2))) < eps/4``.
-Intros.
-Assert H8 := (H2 h H4 H5).
-Assert H9 := (H3 h H6).
-Apply Rle_lt_trans with ``(Rabsolu ((f1 x)/((f2 x)*(f2 (x+h)))))*(Rabsolu (((Rsqr (f2 x))*eps)/(8*(f1 x))))``.
-Rewrite Rabsolu_mult.
-Apply Rle_monotony.
-Apply Rabsolu_pos.
-Left; Apply H8.
-Apply Rlt_le_trans with ``(Rabsolu (2*(f1 x)/((f2 x)*(f2 x))))*(Rabsolu (((Rsqr (f2 x))*eps)/(8*(f1 x))))``.
-Apply Rlt_monotony_r.
-Apply Rabsolu_pos_lt.
-Unfold Rdiv; Unfold Rsqr; Repeat Apply prod_neq_R0; Try Assumption.
-Red; Intro H10; Rewrite H10 in H; Elim (Rlt_antirefl ? H).
-Apply Rinv_neq_R0; Apply prod_neq_R0; DiscrR Orelse Assumption.
-Unfold Rdiv.
-Repeat Rewrite Rinv_Rmult; Try Assumption.
-Repeat Rewrite Rabsolu_mult.
-Replace ``(Rabsolu 2)`` with ``2``.
-Rewrite (Rmult_sym ``2``).
-Replace ``(Rabsolu (f1 x))*((Rabsolu (/(f2 x)))*(Rabsolu (/(f2 x))))*2`` with ``(Rabsolu (f1 x))*((Rabsolu (/(f2 x)))*((Rabsolu (/(f2 x)))*2))``; [Idtac | Ring].
-Repeat Apply Rlt_monotony.
-Apply Rabsolu_pos_lt; Assumption.
-Apply Rabsolu_pos_lt; Apply Rinv_neq_R0; Assumption.
-Repeat Rewrite Rabsolu_Rinv; Assumption Orelse Idtac.
-Rewrite <- (Rmult_sym ``2``).
-Unfold Rdiv in H9; Exact H9.
-Symmetry; Apply Rabsolu_right; Left; Sup0.
-Right.
-Unfold Rsqr Rdiv.
-Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR.
-Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR.
-Repeat Rewrite Rabsolu_mult.
-Repeat Rewrite Rabsolu_Rinv; Try Assumption Orelse DiscrR.
-Replace (Rabsolu eps) with eps.
-Replace ``(Rabsolu (8))`` with ``8``.
-Replace ``(Rabsolu 2)`` with ``2``.
-Replace ``8`` with ``4*2``; [Idtac | Ring].
-Rewrite Rinv_Rmult; DiscrR.
-Replace ``2*((Rabsolu (f1 x))*(/(Rabsolu (f2 x))*/(Rabsolu (f2 x))))*((Rabsolu (f2 x))*(Rabsolu (f2 x))*eps*(/4*/2*/(Rabsolu (f1 x))))`` with ``eps*/4*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*((Rabsolu (f1 x))*/(Rabsolu (f1 x)))*(2*/2)``; [Idtac | Ring].
-Repeat Rewrite <- Rinv_r_sym; Try DiscrR Orelse (Apply Rabsolu_no_R0; Assumption).
-Ring.
-Symmetry; Apply Rabsolu_right; Left; Sup0.
-Symmetry; Apply Rabsolu_right; Left; Sup.
-Symmetry; Apply Rabsolu_right; Left; Assumption.
+Lemma maj_term3 :
+ forall (x h eps l2 alp_f2:R) (eps_f2 alp_f2d:posreal) 
+   (f1 f2:R -> R),
+   0 < eps ->
+   f2 x <> 0 ->
+   f2 (x + h) <> 0 ->
+   (forall h:R,
+      h <> 0 ->
+      Rabs h < alp_f2d ->
+      Rabs ((f2 (x + h) - f2 x) / h - l2) <
+      Rabs (Rsqr (f2 x) * eps / (8 * f1 x))) ->
+   (forall a:R,
+      Rabs a < Rmin eps_f2 alp_f2 -> / Rabs (f2 (x + a)) < 2 / Rabs (f2 x)) ->
+   h <> 0 ->
+   Rabs h < alp_f2d ->
+   Rabs h < Rmin eps_f2 alp_f2 ->
+   f1 x <> 0 ->
+   Rabs (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) <
+   eps / 4.
+intros.
+assert (H8 := H2 h H4 H5).
+assert (H9 := H3 h H6).
+apply Rle_lt_trans with
+ (Rabs (f1 x / (f2 x * f2 (x + h))) * Rabs (Rsqr (f2 x) * eps / (8 * f1 x))).
+rewrite Rabs_mult.
+apply Rmult_le_compat_l.
+apply Rabs_pos.
+left; apply H8.
+apply Rlt_le_trans with
+ (Rabs (2 * (f1 x / (f2 x * f2 x))) * Rabs (Rsqr (f2 x) * eps / (8 * f1 x))).
+apply Rmult_lt_compat_r.
+apply Rabs_pos_lt.
+unfold Rdiv in |- *; unfold Rsqr in |- *; repeat apply prod_neq_R0;
+ try assumption.
+red in |- *; intro H10; rewrite H10 in H; elim (Rlt_irrefl _ H).
+apply Rinv_neq_0_compat; apply prod_neq_R0; discrR || assumption.
+unfold Rdiv in |- *.
+repeat rewrite Rinv_mult_distr; try assumption.
+repeat rewrite Rabs_mult.
+replace (Rabs 2) with 2.
+rewrite (Rmult_comm 2).
+replace (Rabs (f1 x) * (Rabs (/ f2 x) * Rabs (/ f2 x)) * 2) with
+ (Rabs (f1 x) * (Rabs (/ f2 x) * (Rabs (/ f2 x) * 2))); 
+ [ idtac | ring ].
+repeat apply Rmult_lt_compat_l.
+apply Rabs_pos_lt; assumption.
+apply Rabs_pos_lt; apply Rinv_neq_0_compat; assumption.
+repeat rewrite Rabs_Rinv; assumption || idtac.
+rewrite <- (Rmult_comm 2).
+unfold Rdiv in H9; exact H9.
+symmetry  in |- *; apply Rabs_right; left; prove_sup0.
+right.
+unfold Rsqr, Rdiv in |- *.
+rewrite Rinv_mult_distr; try assumption || discrR.
+rewrite Rinv_mult_distr; try assumption || discrR.
+repeat rewrite Rabs_mult.
+repeat rewrite Rabs_Rinv; try assumption || discrR.
+replace (Rabs eps) with eps.
+replace (Rabs 8) with 8.
+replace (Rabs 2) with 2.
+replace 8 with (4 * 2); [ idtac | ring ].
+rewrite Rinv_mult_distr; discrR.
+replace
+ (2 * (Rabs (f1 x) * (/ Rabs (f2 x) * / Rabs (f2 x))) *
+  (Rabs (f2 x) * Rabs (f2 x) * eps * (/ 4 * / 2 * / Rabs (f1 x)))) with
+ (eps * / 4 * (Rabs (f2 x) * / Rabs (f2 x)) * (Rabs (f2 x) * / Rabs (f2 x)) *
+  (Rabs (f1 x) * / Rabs (f1 x)) * (2 * / 2)); [ idtac | ring ].
+repeat rewrite <- Rinv_r_sym; try discrR || (apply Rabs_no_R0; assumption).
+ring.
+symmetry  in |- *; apply Rabs_right; left; prove_sup0.
+symmetry  in |- *; apply Rabs_right; left; prove_sup.
+symmetry  in |- *; apply Rabs_right; left; assumption.
 Qed.
 
-Lemma maj_term4 : (x,h,eps,l2,alp_f2,alp_f2c:R;eps_f2:posreal;f1,f2:R->R) ``0 < eps`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ((a:R)``(Rabsolu a) < alp_f2c`` -> ``(Rabsolu ((f2 (x+a))-(f2 x))) < (Rabsolu (((Rsqr (f2 x))*(f2 x)*eps)/(8*(f1 x)*l2)))``)  -> ((a:R)``(Rabsolu a) < (Rmin eps_f2 alp_f2)``->``/(Rabsolu (f2 (x+a))) < 2/(Rabsolu (f2 x))``) -> ``h<>0`` -> ``(Rabsolu h)<alp_f2c`` -> ``(Rabsolu h) < (Rmin eps_f2 alp_f2)`` -> ``(f1 x)<>0`` -> ``l2<>0`` -> ``(Rabsolu ((l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))*((f2 (x+h))-(f2 x)))) < eps/4``.
-Intros.
-Assert H9 := (H2 h H5).
-Assert H10 := (H3 h H6).
-Apply Rle_lt_trans with ``(Rabsolu ((l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))))*(Rabsolu (((Rsqr (f2 x))*(f2 x)*eps)/(8*(f1 x)*l2)))``.
-Rewrite Rabsolu_mult.
-Apply Rle_monotony.
-Apply Rabsolu_pos.
-Left; Apply H9.
-Apply Rlt_le_trans with ``(Rabsolu (2*l2*(f1 x)/((Rsqr (f2 x))*(f2 x))))*(Rabsolu (((Rsqr (f2 x))*(f2 x)*eps)/(8*(f1 x)*l2)))``.
-Apply Rlt_monotony_r.
-Apply Rabsolu_pos_lt.
-Unfold Rdiv; Unfold Rsqr; Repeat Apply prod_neq_R0; Assumption Orelse Idtac.
-Red; Intro H11; Rewrite H11 in H; Elim (Rlt_antirefl ? H).
-Apply Rinv_neq_R0; Apply prod_neq_R0.
-Apply prod_neq_R0.
-DiscrR.
-Assumption.
-Assumption.
-Unfold Rdiv.
-Repeat Rewrite Rinv_Rmult; Try Assumption Orelse (Unfold Rsqr; Apply prod_neq_R0; Assumption).
-Repeat Rewrite Rabsolu_mult.
-Replace ``(Rabsolu 2)`` with ``2``.
-Replace ``2*(Rabsolu l2)*((Rabsolu (f1 x))*((Rabsolu (/(Rsqr (f2 x))))*(Rabsolu (/(f2 x)))))`` with ``(Rabsolu l2)*((Rabsolu (f1 x))*((Rabsolu (/(Rsqr (f2 x))))*((Rabsolu (/(f2 x)))*2)))``; [Idtac | Ring].
-Replace ``(Rabsolu l2)*(Rabsolu (f1 x))*((Rabsolu (/(Rsqr (f2 x))))*(Rabsolu (/(f2 (x+h)))))`` with ``(Rabsolu l2)*((Rabsolu (f1 x))*(((Rabsolu (/(Rsqr (f2 x))))*(Rabsolu (/(f2 (x+h)))))))``; [Idtac | Ring].
-Repeat Apply Rlt_monotony.
-Apply Rabsolu_pos_lt; Assumption.
-Apply Rabsolu_pos_lt; Assumption.
-Apply Rabsolu_pos_lt; Apply Rinv_neq_R0; Unfold Rsqr; Apply prod_neq_R0;  Assumption.
-Repeat Rewrite Rabsolu_Rinv; [Idtac | Assumption | Assumption].
-Rewrite <- (Rmult_sym ``2``).
-Unfold Rdiv in H10; Exact H10.
-Symmetry; Apply Rabsolu_right; Left; Sup0.
-Right; Unfold Rsqr Rdiv.
-Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR.
-Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR.
-Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR.
-Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR.
-Repeat Rewrite Rabsolu_mult.
-Repeat Rewrite Rabsolu_Rinv; Try Assumption Orelse DiscrR.
-Replace (Rabsolu eps) with eps.
-Replace ``(Rabsolu (8))`` with ``8``.
-Replace ``(Rabsolu 2)`` with ``2``.
-Replace ``8`` with ``4*2``; [Idtac | Ring].
-Rewrite Rinv_Rmult; DiscrR.
-Replace ``2*(Rabsolu l2)*((Rabsolu (f1 x))*(/(Rabsolu (f2 x))*/(Rabsolu (f2 x))*/(Rabsolu (f2 x))))*((Rabsolu (f2 x))*(Rabsolu (f2 x))*(Rabsolu (f2 x))*eps*(/4*/2*/(Rabsolu (f1 x))*/(Rabsolu l2)))`` with ``eps*/4*((Rabsolu l2)*/(Rabsolu l2))*((Rabsolu (f1 x))*/(Rabsolu (f1 x)))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*(2*/2)``; [Idtac | Ring].
-Repeat Rewrite <- Rinv_r_sym; Try DiscrR Orelse (Apply Rabsolu_no_R0; Assumption).
-Ring.
-Symmetry; Apply Rabsolu_right; Left; Sup0.
-Symmetry; Apply Rabsolu_right; Left; Sup.
-Symmetry; Apply Rabsolu_right; Left; Assumption.
-Apply prod_neq_R0; Assumption Orelse DiscrR.
-Apply prod_neq_R0; Assumption.
+Lemma maj_term4 :
+ forall (x h eps l2 alp_f2 alp_f2c:R) (eps_f2:posreal) 
+   (f1 f2:R -> R),
+   0 < eps ->
+   f2 x <> 0 ->
+   f2 (x + h) <> 0 ->
+   (forall a:R,
+      Rabs a < alp_f2c ->
+      Rabs (f2 (x + a) - f2 x) <
+      Rabs (Rsqr (f2 x) * f2 x * eps / (8 * f1 x * l2))) ->
+   (forall a:R,
+      Rabs a < Rmin eps_f2 alp_f2 -> / Rabs (f2 (x + a)) < 2 / Rabs (f2 x)) ->
+   h <> 0 ->
+   Rabs h < alp_f2c ->
+   Rabs h < Rmin eps_f2 alp_f2 ->
+   f1 x <> 0 ->
+   l2 <> 0 ->
+   Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x)) <
+   eps / 4.
+intros.
+assert (H9 := H2 h H5).
+assert (H10 := H3 h H6).
+apply Rle_lt_trans with
+ (Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h))) *
+  Rabs (Rsqr (f2 x) * f2 x * eps / (8 * f1 x * l2))).
+rewrite Rabs_mult.
+apply Rmult_le_compat_l.
+apply Rabs_pos.
+left; apply H9.
+apply Rlt_le_trans with
+ (Rabs (2 * l2 * (f1 x / (Rsqr (f2 x) * f2 x))) *
+  Rabs (Rsqr (f2 x) * f2 x * eps / (8 * f1 x * l2))).
+apply Rmult_lt_compat_r.
+apply Rabs_pos_lt.
+unfold Rdiv in |- *; unfold Rsqr in |- *; repeat apply prod_neq_R0;
+ assumption || idtac.
+red in |- *; intro H11; rewrite H11 in H; elim (Rlt_irrefl _ H).
+apply Rinv_neq_0_compat; apply prod_neq_R0.
+apply prod_neq_R0.
+discrR.
+assumption.
+assumption.
+unfold Rdiv in |- *.
+repeat rewrite Rinv_mult_distr;
+ try assumption || (unfold Rsqr in |- *; apply prod_neq_R0; assumption).
+repeat rewrite Rabs_mult.
+replace (Rabs 2) with 2.
+replace
+ (2 * Rabs l2 * (Rabs (f1 x) * (Rabs (/ Rsqr (f2 x)) * Rabs (/ f2 x)))) with
+ (Rabs l2 * (Rabs (f1 x) * (Rabs (/ Rsqr (f2 x)) * (Rabs (/ f2 x) * 2))));
+ [ idtac | ring ].
+replace
+ (Rabs l2 * Rabs (f1 x) * (Rabs (/ Rsqr (f2 x)) * Rabs (/ f2 (x + h)))) with
+ (Rabs l2 * (Rabs (f1 x) * (Rabs (/ Rsqr (f2 x)) * Rabs (/ f2 (x + h)))));
+ [ idtac | ring ].
+repeat apply Rmult_lt_compat_l.
+apply Rabs_pos_lt; assumption.
+apply Rabs_pos_lt; assumption.
+apply Rabs_pos_lt; apply Rinv_neq_0_compat; unfold Rsqr in |- *;
+ apply prod_neq_R0; assumption.
+repeat rewrite Rabs_Rinv; [ idtac | assumption | assumption ].
+rewrite <- (Rmult_comm 2).
+unfold Rdiv in H10; exact H10.
+symmetry  in |- *; apply Rabs_right; left; prove_sup0.
+right; unfold Rsqr, Rdiv in |- *.
+rewrite Rinv_mult_distr; try assumption || discrR.
+rewrite Rinv_mult_distr; try assumption || discrR.
+rewrite Rinv_mult_distr; try assumption || discrR.
+rewrite Rinv_mult_distr; try assumption || discrR.
+repeat rewrite Rabs_mult.
+repeat rewrite Rabs_Rinv; try assumption || discrR.
+replace (Rabs eps) with eps.
+replace (Rabs 8) with 8.
+replace (Rabs 2) with 2.
+replace 8 with (4 * 2); [ idtac | ring ].
+rewrite Rinv_mult_distr; discrR.
+replace
+ (2 * Rabs l2 *
+  (Rabs (f1 x) * (/ Rabs (f2 x) * / Rabs (f2 x) * / Rabs (f2 x))) *
+  (Rabs (f2 x) * Rabs (f2 x) * Rabs (f2 x) * eps *
+   (/ 4 * / 2 * / Rabs (f1 x) * / Rabs l2))) with
+ (eps * / 4 * (Rabs l2 * / Rabs l2) * (Rabs (f1 x) * / Rabs (f1 x)) *
+  (Rabs (f2 x) * / Rabs (f2 x)) * (Rabs (f2 x) * / Rabs (f2 x)) *
+  (Rabs (f2 x) * / Rabs (f2 x)) * (2 * / 2)); [ idtac | ring ].
+repeat rewrite <- Rinv_r_sym; try discrR || (apply Rabs_no_R0; assumption).
+ring.
+symmetry  in |- *; apply Rabs_right; left; prove_sup0.
+symmetry  in |- *; apply Rabs_right; left; prove_sup.
+symmetry  in |- *; apply Rabs_right; left; assumption.
+apply prod_neq_R0; assumption || discrR.
+apply prod_neq_R0; assumption.
 Qed.
 
-Lemma D_x_no_cond : (x,a:R) ``a<>0`` -> (D_x no_cond x ``x+a``).
-Intros.
-Unfold D_x no_cond.
-Split.
-Trivial.
-Apply Rminus_not_eq.
-Unfold Rminus.
-Rewrite Ropp_distr1.
-Rewrite <- Rplus_assoc.
-Rewrite Rplus_Ropp_r.
-Rewrite Rplus_Ol.
-Apply Ropp_neq; Assumption.
+Lemma D_x_no_cond : forall x a:R, a <> 0 -> D_x no_cond x (x + a).
+intros.
+unfold D_x, no_cond in |- *.
+split.
+trivial.
+apply Rminus_not_eq.
+unfold Rminus in |- *.
+rewrite Ropp_plus_distr.
+rewrite <- Rplus_assoc.
+rewrite Rplus_opp_r.
+rewrite Rplus_0_l.
+apply Ropp_neq_0_compat; assumption.
 Qed.
 
-Lemma Rabsolu_4 : (a,b,c,d:R) ``(Rabsolu (a+b+c+d)) <= (Rabsolu a) + (Rabsolu b) + (Rabsolu c) + (Rabsolu d)``.
-Intros.
-Apply Rle_trans with ``(Rabsolu (a+b)) + (Rabsolu (c+d))``.
-Replace ``a+b+c+d`` with ``(a+b)+(c+d)``; [Apply Rabsolu_triang | Ring].
-Apply Rle_trans with ``(Rabsolu a) + (Rabsolu b) + (Rabsolu (c+d))``.
-Apply Rle_compatibility_r.
-Apply Rabsolu_triang.
-Repeat Rewrite Rplus_assoc; Repeat Apply Rle_compatibility.
-Apply Rabsolu_triang.
+Lemma Rabs_4 :
+ forall a b c d:R, Rabs (a + b + c + d) <= Rabs a + Rabs b + Rabs c + Rabs d.
+intros.
+apply Rle_trans with (Rabs (a + b) + Rabs (c + d)).
+replace (a + b + c + d) with (a + b + (c + d)); [ apply Rabs_triang | ring ].
+apply Rle_trans with (Rabs a + Rabs b + Rabs (c + d)).
+apply Rplus_le_compat_r.
+apply Rabs_triang.
+repeat rewrite Rplus_assoc; repeat apply Rplus_le_compat_l.
+apply Rabs_triang.
 Qed.
 
-Lemma Rlt_4 : (a,b,c,d,e,f,g,h:R) ``a < b`` -> ``c < d`` -> ``e < f `` -> ``g < h`` -> ``a+c+e+g < b+d+f+h``.
-Intros; Apply Rlt_trans with ``b+c+e+g``.
-Repeat Apply Rlt_compatibility_r; Assumption.
-Repeat Rewrite Rplus_assoc; Apply Rlt_compatibility.
-Apply Rlt_trans with ``d+e+g``.
-Rewrite Rplus_assoc; Apply Rlt_compatibility_r; Assumption.
-Rewrite Rplus_assoc; Apply Rlt_compatibility; Apply Rlt_trans with ``f+g``.
-Apply Rlt_compatibility_r; Assumption.
-Apply Rlt_compatibility; Assumption.
+Lemma Rlt_4 :
+ forall a b c d e f g h:R,
+   a < b -> c < d -> e < f -> g < h -> a + c + e + g < b + d + f + h.
+intros; apply Rlt_trans with (b + c + e + g).
+repeat apply Rplus_lt_compat_r; assumption.
+repeat rewrite Rplus_assoc; apply Rplus_lt_compat_l.
+apply Rlt_trans with (d + e + g).
+rewrite Rplus_assoc; apply Rplus_lt_compat_r; assumption.
+rewrite Rplus_assoc; apply Rplus_lt_compat_l; apply Rlt_trans with (f + g).
+apply Rplus_lt_compat_r; assumption.
+apply Rplus_lt_compat_l; assumption.
 Qed.
 
-Lemma Rmin_2 : (a,b,c:R) ``a < b`` -> ``a < c`` -> ``a < (Rmin b c)``.
-Intros; Unfold Rmin; Case (total_order_Rle b c); Intro; Assumption.
+Lemma Rmin_2 : forall a b c:R, a < b -> a < c -> a < Rmin b c.
+intros; unfold Rmin in |- *; case (Rle_dec b c); intro; assumption.
 Qed.
 
-Lemma quadruple : (x:R) ``4*x == x + x + x + x``.
-Intro; Ring.
+Lemma quadruple : forall x:R, 4 * x = x + x + x + x.
+intro; ring.
 Qed.
 
-Lemma quadruple_var : (x:R) `` x == x/4 + x/4 + x/4 + x/4``.
-Intro; Rewrite <- quadruple.
-Unfold Rdiv; Rewrite <- Rmult_assoc; Rewrite Rinv_r_simpl_m; DiscrR.
-Reflexivity.
+Lemma quadruple_var : forall x:R, x = x / 4 + x / 4 + x / 4 + x / 4.
+intro; rewrite <- quadruple.
+unfold Rdiv in |- *; rewrite <- Rmult_assoc; rewrite Rinv_r_simpl_m; discrR.
+reflexivity.
 Qed.
 
 (**********)
-Lemma continuous_neq_0 : (f:R->R; x0:R) (continuity_pt f x0) -> ~``(f x0)==0`` -> (EXT eps : posreal | (h:R) ``(Rabsolu h) < eps`` -> ~``(f (x0+h))==0``).
-Intros; Unfold continuity_pt in H; Unfold continue_in in H; Unfold limit1_in in H; Unfold limit_in in H; Elim (H ``(Rabsolu ((f x0)/2))``).
-Intros; Elim H1; Intros.
-Exists (mkposreal x H2).
-Intros; Assert H5 := (H3 ``x0+h``).
-Cut ``(dist R_met (x0+h) x0) < x`` -> ``(dist R_met (f (x0+h)) (f x0)) < (Rabsolu ((f x0)/2))``.
-Unfold dist; Simpl; Unfold R_dist; Replace ``x0+h-x0`` with h.
-Intros; Assert H7 := (H6 H4).
-Red; Intro.
-Rewrite H8 in H7; Unfold Rminus in H7; Rewrite Rplus_Ol in H7; Rewrite Rabsolu_Ropp in H7; Unfold Rdiv in H7; Rewrite Rabsolu_mult in H7; Pattern 1 ``(Rabsolu (f x0)) `` in H7; Rewrite <- Rmult_1r in H7.
-Cut ``0<(Rabsolu (f x0))``.
-Intro; Assert H10 := (Rlt_monotony_contra ? ? ? H9 H7).
-Cut ``(Rabsolu (/2))==/2``.
-Assert Hyp:``0<2``.
-Sup0.
-Intro; Rewrite H11 in H10; Assert H12 := (Rlt_monotony ``2`` ? ? Hyp H10); Rewrite Rmult_1r in H12; Rewrite <- Rinv_r_sym in H12; [Idtac | DiscrR].
-Cut (Rlt (IZR `1`) (IZR `2`)).
-Unfold IZR; Unfold INR convert; Simpl; Intro; Elim (Rlt_antirefl ``1`` (Rlt_trans ? ? ? H13 H12)).
-Apply IZR_lt; Omega.
-Unfold Rabsolu; Case (case_Rabsolu ``/2``); Intro.
-Assert Hyp:``0<2``.
-Sup0.
-Assert H11 := (Rlt_monotony ``2`` ? ? Hyp r); Rewrite Rmult_Or in H11; Rewrite <- Rinv_r_sym in H11; [Idtac | DiscrR].
-Elim (Rlt_antirefl ``0`` (Rlt_trans ? ? ? Rlt_R0_R1 H11)).
-Reflexivity.
-Apply (Rabsolu_pos_lt ? H0).
-Ring.
-Assert H6 := (Req_EM ``x0`` ``x0+h``); Elim H6; Intro.
-Intro; Rewrite <- H7; Unfold dist R_met; Unfold R_dist; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Apply Rabsolu_pos_lt.
-Unfold Rdiv; Apply prod_neq_R0; [Assumption | Apply Rinv_neq_R0; DiscrR].
-Intro; Apply H5.
-Split.
-Unfold D_x no_cond.
-Split; Trivial Orelse Assumption.
-Assumption.
-Change ``0 < (Rabsolu ((f x0)/2))``.
-Apply Rabsolu_pos_lt; Unfold Rdiv; Apply prod_neq_R0.
-Assumption.
-Apply Rinv_neq_R0; DiscrR.
-Qed.
+Lemma continuous_neq_0 :
+ forall (f:R -> R) (x0:R),
+   continuity_pt f x0 ->
+   f x0 <> 0 ->
+    exists eps : posreal | (forall h:R, Rabs h < eps -> f (x0 + h) <> 0).
+intros; unfold continuity_pt in H; unfold continue_in in H;
+ unfold limit1_in in H; unfold limit_in in H; elim (H (Rabs (f x0 / 2))).
+intros; elim H1; intros.
+exists (mkposreal x H2).
+intros; assert (H5 := H3 (x0 + h)).
+cut
+ (dist R_met (x0 + h) x0 < x ->
+  dist R_met (f (x0 + h)) (f x0) < Rabs (f x0 / 2)).
+unfold dist in |- *; simpl in |- *; unfold R_dist in |- *;
+ replace (x0 + h - x0) with h.
+intros; assert (H7 := H6 H4).
+red in |- *; intro.
+rewrite H8 in H7; unfold Rminus in H7; rewrite Rplus_0_l in H7;
+ rewrite Rabs_Ropp in H7; unfold Rdiv in H7; rewrite Rabs_mult in H7;
+ pattern (Rabs (f x0)) at 1 in H7; rewrite <- Rmult_1_r in H7.
+cut (0 < Rabs (f x0)).
+intro; assert (H10 := Rmult_lt_reg_l _ _ _ H9 H7).
+cut (Rabs (/ 2) = / 2).
+assert (Hyp : 0 < 2).
+prove_sup0.
+intro; rewrite H11 in H10; assert (H12 := Rmult_lt_compat_l 2 _ _ Hyp H10);
+ rewrite Rmult_1_r in H12; rewrite <- Rinv_r_sym in H12; 
+ [ idtac | discrR ].
+cut (IZR 1 < IZR 2).
+unfold IZR in |- *; unfold INR, nat_of_P in |- *; simpl in |- *; intro;
+ elim (Rlt_irrefl 1 (Rlt_trans _ _ _ H13 H12)).
+apply IZR_lt; omega.
+unfold Rabs in |- *; case (Rcase_abs (/ 2)); intro.
+assert (Hyp : 0 < 2).
+prove_sup0.
+assert (H11 := Rmult_lt_compat_l 2 _ _ Hyp r); rewrite Rmult_0_r in H11;
+ rewrite <- Rinv_r_sym in H11; [ idtac | discrR ].
+elim (Rlt_irrefl 0 (Rlt_trans _ _ _ Rlt_0_1 H11)).
+reflexivity.
+apply (Rabs_pos_lt _ H0).
+ring.
+assert (H6 := Req_dec x0 (x0 + h)); elim H6; intro.
+intro; rewrite <- H7; unfold dist, R_met in |- *; unfold R_dist in |- *;
+ unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0;
+ apply Rabs_pos_lt.
+unfold Rdiv in |- *; apply prod_neq_R0;
+ [ assumption | apply Rinv_neq_0_compat; discrR ].
+intro; apply H5.
+split.
+unfold D_x, no_cond in |- *.
+split; trivial || assumption.
+assumption.
+change (0 < Rabs (f x0 / 2)) in |- *.
+apply Rabs_pos_lt; unfold Rdiv in |- *; apply prod_neq_R0.
+assumption.
+apply Rinv_neq_0_compat; discrR.
+Qed.
\ No newline at end of file