diff options
Diffstat (limited to 'theories7/Reals/Ranalysis2.v')
| -rw-r--r-- | theories7/Reals/Ranalysis2.v | 302 |
1 files changed, 0 insertions, 302 deletions
diff --git a/theories7/Reals/Ranalysis2.v b/theories7/Reals/Ranalysis2.v deleted file mode 100644 index 35fa58d5..00000000 --- a/theories7/Reals/Ranalysis2.v +++ /dev/null @@ -1,302 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Ranalysis2.v,v 1.1.2.1 2004/07/16 19:31:33 herbelin Exp $ i*) - -Require Rbase. -Require Rfunctions. -Require Ranalysis1. -V7only [Import R_scope.]. 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. -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. -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. -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. -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. -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. -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. -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. -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. -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. -Qed. - -Lemma quadruple : (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. -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. |