diff options
Diffstat (limited to 'theories/Reals/Ranalysis5.v')
| -rw-r--r-- | theories/Reals/Ranalysis5.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v index d876b5d8e..0614f3998 100644 --- a/theories/Reals/Ranalysis5.v +++ b/theories/Reals/Ranalysis5.v @@ -695,7 +695,7 @@ intros f g lb ub x Prf g_cont_pur lb_lt_ub x_encad Prg_incr f_eq_g df_neq. exists deltatemp ; exact Htemp. elim (Hf_deriv eps eps_pos). intros deltatemp Htemp. - red in Hlinv ; red in Hlinv ; simpl dist in Hlinv ; unfold R_dist in Hlinv. + red in Hlinv ; red in Hlinv ; unfold dist in Hlinv ; unfold R_dist in Hlinv. assert (Hlinv' := Hlinv (fun h => (f (y+h) - f y)/h) (fun h => h <>0) l 0). unfold limit1_in, limit_in, dist in Hlinv' ; simpl in Hlinv'. unfold R_dist in Hlinv'. assert (Premisse : (forall eps : R, |