← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Reals/Ranalysis3.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Reals/Ranalysis3.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: Ranalysis3.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
10
 
 
11
Require Import Rbase.
 
12
Require Import Rfunctions.
 
13
Require Import Ranalysis1.
 
14
Require Import Ranalysis2.
 
15
Open Local Scope R_scope.
 
16
 
 
17
(** Division *)
 
18
Theorem derivable_pt_lim_div :
 
19
  forall (f1 f2:R -> R) (x l1 l2:R),
 
20
    derivable_pt_lim f1 x l1 ->
 
21
    derivable_pt_lim f2 x l2 ->
 
22
    f2 x <> 0 ->
 
23
    derivable_pt_lim (f1 / f2) x ((l1 * f2 x - l2 * f1 x) / Rsqr (f2 x)).
 
24
Proof.
 
25
  intros f1 f2 x l1 l2 H H0 H1.
 
26
  cut (derivable_pt f2 x);
 
27
    [ intro X | unfold derivable_pt in |- *; exists l2; exact H0 ].
 
28
  assert (H2 := continuous_neq_0 _ _ (derivable_continuous_pt _ _ X) H1).
 
29
  elim H2; clear H2; intros eps_f2 H2.
 
30
  unfold div_fct in |- *.
 
31
  assert (H3 := derivable_continuous_pt _ _ X).
 
32
  unfold continuity_pt in H3; unfold continue_in in H3; unfold limit1_in in H3;
 
33
    unfold limit_in in H3; unfold dist in H3.
 
34
  simpl in H3; unfold R_dist in H3.
 
35
  elim (H3 (Rabs (f2 x) / 2));
 
36
    [ idtac
 
37
      | unfold Rdiv in |- *; change (0 < Rabs (f2 x) * / 2) in |- *;
 
38
        apply Rmult_lt_0_compat;
 
39
          [ apply Rabs_pos_lt; assumption | apply Rinv_0_lt_compat; prove_sup0 ] ].
 
40
  clear H3; intros alp_f2 H3.
 
41
  cut
 
42
    (forall x0:R,
 
43
      Rabs (x0 - x) < alp_f2 -> Rabs (f2 x0 - f2 x) < Rabs (f2 x) / 2).
 
44
  intro H4.
 
45
  cut (forall a:R, Rabs (a - x) < alp_f2 -> Rabs (f2 x) / 2 < Rabs (f2 a)).
 
46
  intro H5.
 
47
  cut
 
48
    (forall a:R,
 
49
      Rabs a < Rmin eps_f2 alp_f2 -> / Rabs (f2 (x + a)) < 2 / Rabs (f2 x)).
 
50
  intro Maj.
 
51
  unfold derivable_pt_lim in |- *; intros.
 
52
  elim (H (Rabs (eps * f2 x / 8)));
 
53
    [ idtac
 
54
      | unfold Rdiv in |- *; change (0 < Rabs (eps * f2 x * / 8)) in |- *;
 
55
        apply Rabs_pos_lt; repeat apply prod_neq_R0;
 
56
          [ red in |- *; intro H7; rewrite H7 in H6; elim (Rlt_irrefl _ H6)
 
57
            | assumption
 
58
            | apply Rinv_neq_0_compat; discrR ] ].
 
59
  intros alp_f1d H7.
 
60
  case (Req_dec (f1 x) 0); intro.
 
61
  case (Req_dec l1 0); intro.
 
62
(***********************************)
 
63
(*              Cas n� 1           *)
 
64
(*           (f1 x)=0  l1 =0       *)
 
65
(***********************************)
 
66
  cut (0 < Rmin eps_f2 (Rmin alp_f2 alp_f1d));
 
67
    [ intro
 
68
      | repeat apply Rmin_pos;
 
69
        [ apply (cond_pos eps_f2)
 
70
          | elim H3; intros; assumption
 
71
          | apply (cond_pos alp_f1d) ] ].
 
72
  exists (mkposreal (Rmin eps_f2 (Rmin alp_f2 alp_f1d)) H10).
 
73
  simpl in |- *; intros.
 
74
  assert (H13 := Rlt_le_trans _ _ _ H12 (Rmin_r _ _)).
 
75
  assert (H14 := Rlt_le_trans _ _ _ H12 (Rmin_l _ _)).
 
76
  assert (H15 := Rlt_le_trans _ _ _ H13 (Rmin_r _ _)).
 
77
  assert (H16 := Rlt_le_trans _ _ _ H13 (Rmin_l _ _)).
 
78
  assert (H17 := H7 _ H11 H15).
 
79
  rewrite formule; [ idtac | assumption | assumption | apply H2; apply H14 ].
 
80
  apply Rle_lt_trans with
 
81
    (Rabs (/ f2 (x + h) * ((f1 (x + h) - f1 x) / h - l1)) +
 
82
      Rabs (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) +
 
83
      Rabs (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) +
 
84
      Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x))).
 
85
  unfold Rminus in |- *.
 
86
  rewrite <-
 
87
    (Rabs_Ropp (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) + - f2 x) / h + - l2)))
 
88
    .
 
89
  apply Rabs_4.
 
90
  repeat rewrite Rabs_mult.
 
91
  apply Rlt_le_trans with (eps / 4 + eps / 4 + eps / 4 + eps / 4).
 
92
  cut (Rabs (/ f2 (x + h)) * Rabs ((f1 (x + h) - f1 x) / h - l1) < eps / 4).
 
93
  cut (Rabs (l1 / (f2 x * f2 (x + h))) * Rabs (f2 x - f2 (x + h)) < eps / 4).
 
94
  cut
 
95
    (Rabs (f1 x / (f2 x * f2 (x + h))) * Rabs ((f2 (x + h) - f2 x) / h - l2) <
 
96
      eps / 4).
 
97
  cut
 
98
    (Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h))) * Rabs (f2 (x + h) - f2 x) <
 
99
      eps / 4).
 
100
  intros.
 
101
  apply Rlt_4; assumption.
 
102
  rewrite H8.
 
103
  unfold Rdiv in |- *; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
 
104
  rewrite Rabs_R0; rewrite Rmult_0_l.
 
105
  apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup ].
 
106
  rewrite H8.
 
107
  unfold Rdiv in |- *; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
 
108
  rewrite Rabs_R0; rewrite Rmult_0_l.
 
109
  apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup ].
 
110
  rewrite H9.
 
111
  unfold Rdiv in |- *; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
 
112
  rewrite Rabs_R0; rewrite Rmult_0_l.
 
113
  apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup ].
 
114
  rewrite <- Rabs_mult.
 
115
  apply (maj_term1 x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2);
 
116
    try assumption || apply H2.
 
117
  apply H14.
 
118
  apply Rmin_2; assumption.
 
119
  right; symmetry  in |- *; apply quadruple_var.
 
120
(***********************************)
 
121
(*              Cas n� 2           *)
 
122
(*           (f1 x)=0  l1<>0       *)
 
123
(***********************************)
 
124
  assert (H10 := derivable_continuous_pt _ _ X).
 
125
  unfold continuity_pt in H10.
 
126
  unfold continue_in in H10.
 
127
  unfold limit1_in in H10.
 
128
  unfold limit_in in H10.
 
129
  unfold dist in H10.
 
130
  simpl in H10.
 
131
  unfold R_dist in H10.
 
132
  elim (H10 (Rabs (eps * Rsqr (f2 x) / (8 * l1)))).
 
133
  clear H10; intros alp_f2t2 H10.
 
134
  cut
 
135
    (forall a:R,
 
136
      Rabs a < alp_f2t2 ->
 
137
      Rabs (f2 (x + a) - f2 x) < Rabs (eps * Rsqr (f2 x) / (8 * l1))).
 
138
  intro H11.
 
139
  cut (0 < Rmin (Rmin eps_f2 alp_f1d) (Rmin alp_f2 alp_f2t2)).
 
140
  intro.
 
141
  exists (mkposreal (Rmin (Rmin eps_f2 alp_f1d) (Rmin alp_f2 alp_f2t2)) H12).
 
142
  simpl in |- *.
 
143
  intros.
 
144
  assert (H15 := Rlt_le_trans _ _ _ H14 (Rmin_r _ _)).
 
145
  assert (H16 := Rlt_le_trans _ _ _ H14 (Rmin_l _ _)).
 
146
  assert (H17 := Rlt_le_trans _ _ _ H15 (Rmin_l _ _)).
 
147
  assert (H18 := Rlt_le_trans _ _ _ H15 (Rmin_r _ _)).
 
148
  assert (H19 := Rlt_le_trans _ _ _ H16 (Rmin_l _ _)).
 
149
  assert (H20 := Rlt_le_trans _ _ _ H16 (Rmin_r _ _)).
 
150
  clear H14 H15 H16.
 
151
  rewrite formule; try assumption.
 
152
  apply Rle_lt_trans with
 
153
    (Rabs (/ f2 (x + h) * ((f1 (x + h) - f1 x) / h - l1)) +
 
154
      Rabs (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) +
 
155
      Rabs (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) +
 
156
      Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x))).
 
157
  unfold Rminus in |- *.
 
158
  rewrite <-
 
159
    (Rabs_Ropp (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) + - f2 x) / h + - l2)))
 
160
    .
 
161
  apply Rabs_4.
 
162
  repeat rewrite Rabs_mult.
 
163
  apply Rlt_le_trans with (eps / 4 + eps / 4 + eps / 4 + eps / 4).
 
164
  cut (Rabs (/ f2 (x + h)) * Rabs ((f1 (x + h) - f1 x) / h - l1) < eps / 4).
 
165
  cut (Rabs (l1 / (f2 x * f2 (x + h))) * Rabs (f2 x - f2 (x + h)) < eps / 4).
 
166
  cut
 
167
    (Rabs (f1 x / (f2 x * f2 (x + h))) * Rabs ((f2 (x + h) - f2 x) / h - l2) <
 
168
      eps / 4).
 
169
  cut
 
170
    (Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h))) * Rabs (f2 (x + h) - f2 x) <
 
171
      eps / 4).
 
172
  intros.
 
173
  apply Rlt_4; assumption.
 
174
  rewrite H8.
 
175
  unfold Rdiv in |- *; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
 
176
  rewrite Rabs_R0; rewrite Rmult_0_l.
 
177
  apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup ].
 
178
  rewrite H8.
 
179
  unfold Rdiv in |- *; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
 
180
  rewrite Rabs_R0; rewrite Rmult_0_l.
 
181
  apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup ].
 
182
  rewrite <- Rabs_mult.
 
183
  apply (maj_term2 x h eps l1 alp_f2 alp_f2t2 eps_f2 f2); try assumption.
 
184
  apply H2; assumption.
 
185
  apply Rmin_2; assumption.
 
186
  rewrite <- Rabs_mult.
 
187
  apply (maj_term1 x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2); try assumption.
 
188
  apply H2; assumption.
 
189
  apply Rmin_2; assumption.
 
190
  right; symmetry  in |- *; apply quadruple_var.
 
191
  apply H2; assumption.
 
192
  repeat apply Rmin_pos.
 
193
  apply (cond_pos eps_f2).
 
194
  apply (cond_pos alp_f1d).
 
195
  elim H3; intros; assumption.
 
196
  elim H10; intros; assumption.
 
197
  intros.
 
198
  elim H10; intros.
 
199
  case (Req_dec a 0); intro.
 
200
  rewrite H14; rewrite Rplus_0_r.
 
201
  unfold Rminus in |- *; rewrite Rplus_opp_r.
 
202
  rewrite Rabs_R0.
 
203
  apply Rabs_pos_lt.
 
204
  unfold Rdiv, Rsqr in |- *; repeat rewrite Rmult_assoc.
 
205
  repeat apply prod_neq_R0; try assumption.
 
206
  red in |- *; intro; rewrite H15 in H6; elim (Rlt_irrefl _ H6).
 
207
  apply Rinv_neq_0_compat; repeat apply prod_neq_R0; discrR || assumption.
 
208
  apply H13.
 
209
  split.
 
210
  apply D_x_no_cond; assumption.
 
211
  replace (x + a - x) with a; [ assumption | ring ].
 
212
  change (0 < Rabs (eps * Rsqr (f2 x) / (8 * l1))) in |- *.
 
213
  apply Rabs_pos_lt; unfold Rdiv, Rsqr in |- *; repeat rewrite Rmult_assoc;
 
214
    repeat apply prod_neq_R0.
 
215
  red in |- *; intro; rewrite H11 in H6; elim (Rlt_irrefl _ H6).
 
216
  assumption. 
 
217
  assumption.
 
218
  apply Rinv_neq_0_compat; repeat apply prod_neq_R0;
 
219
    [ discrR | discrR | discrR | assumption ].
 
220
(***********************************)
 
221
(*              Cas n� 3           *)
 
222
(*     (f1 x)<>0  l1=0  l2=0       *)
 
223
(***********************************)
 
224
  case (Req_dec l1 0); intro.
 
225
  case (Req_dec l2 0); intro.
 
226
  elim (H0 (Rabs (Rsqr (f2 x) * eps / (8 * f1 x))));
 
227
    [ idtac
 
228
      | apply Rabs_pos_lt; unfold Rdiv, Rsqr in |- *; repeat rewrite Rmult_assoc;
 
229
        repeat apply prod_neq_R0;
 
230
          [ assumption
 
231
            | assumption
 
232
            | red in |- *; intro; rewrite H11 in H6; elim (Rlt_irrefl _ H6)
 
233
            | apply Rinv_neq_0_compat; repeat apply prod_neq_R0; discrR || assumption ] ].
 
234
  intros alp_f2d H12.
 
235
  cut (0 < Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d alp_f2d)).
 
236
  intro.
 
237
  exists (mkposreal (Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d alp_f2d)) H11).
 
238
  simpl in |- *.
 
239
  intros.
 
240
  assert (H15 := Rlt_le_trans _ _ _ H14 (Rmin_l _ _)).
 
241
  assert (H16 := Rlt_le_trans _ _ _ H14 (Rmin_r _ _)).
 
242
  assert (H17 := Rlt_le_trans _ _ _ H15 (Rmin_l _ _)).
 
243
  assert (H18 := Rlt_le_trans _ _ _ H15 (Rmin_r _ _)).
 
244
  assert (H19 := Rlt_le_trans _ _ _ H16 (Rmin_l _ _)).
 
245
  assert (H20 := Rlt_le_trans _ _ _ H16 (Rmin_r _ _)).
 
246
  clear H15 H16.
 
247
  rewrite formule; try assumption.
 
248
  apply Rle_lt_trans with
 
249
    (Rabs (/ f2 (x + h) * ((f1 (x + h) - f1 x) / h - l1)) +
 
250
      Rabs (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) +
 
251
      Rabs (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) +
 
252
      Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x))).
 
253
  unfold Rminus in |- *.
 
254
  rewrite <-
 
255
    (Rabs_Ropp (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) + - f2 x) / h + - l2)))
 
256
    .
 
257
  apply Rabs_4.
 
258
  repeat rewrite Rabs_mult.
 
259
  apply Rlt_le_trans with (eps / 4 + eps / 4 + eps / 4 + eps / 4).
 
260
  cut (Rabs (/ f2 (x + h)) * Rabs ((f1 (x + h) - f1 x) / h - l1) < eps / 4).
 
261
  cut (Rabs (l1 / (f2 x * f2 (x + h))) * Rabs (f2 x - f2 (x + h)) < eps / 4).
 
262
  cut
 
263
    (Rabs (f1 x / (f2 x * f2 (x + h))) * Rabs ((f2 (x + h) - f2 x) / h - l2) <
 
264
      eps / 4).
 
265
  cut
 
266
    (Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h))) * Rabs (f2 (x + h) - f2 x) <
 
267
      eps / 4).
 
268
  intros.
 
269
  apply Rlt_4; assumption.
 
270
  rewrite H10.
 
271
  unfold Rdiv in |- *; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
 
272
  rewrite Rabs_R0; rewrite Rmult_0_l.
 
273
  apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup ].
 
274
  rewrite <- Rabs_mult.
 
275
  apply (maj_term3 x h eps l2 alp_f2 eps_f2 alp_f2d f1 f2); try assumption.
 
276
  apply H2; assumption.
 
277
  apply Rmin_2; assumption.
 
278
  rewrite H9.
 
279
  unfold Rdiv in |- *; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
 
280
  rewrite Rabs_R0; rewrite Rmult_0_l.
 
281
  apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup ].
 
282
  rewrite <- Rabs_mult.
 
283
  apply (maj_term1 x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2); assumption || idtac.
 
284
  apply H2; assumption.
 
285
  apply Rmin_2; assumption.
 
286
  right; symmetry  in |- *; apply quadruple_var.
 
287
  apply H2; assumption.
 
288
  repeat apply Rmin_pos.
 
289
  apply (cond_pos eps_f2).
 
290
  elim H3; intros; assumption.
 
291
  apply (cond_pos alp_f1d).
 
292
  apply (cond_pos alp_f2d).
 
293
(***********************************)
 
294
(*              Cas n� 4           *)
 
295
(*    (f1 x)<>0  l1=0  l2<>0       *)
 
296
(***********************************)
 
297
  elim (H0 (Rabs (Rsqr (f2 x) * eps / (8 * f1 x))));
 
298
    [ idtac
 
299
      | apply Rabs_pos_lt; unfold Rsqr, Rdiv in |- *;
 
300
        repeat rewrite Rinv_mult_distr; repeat apply prod_neq_R0;
 
301
          try assumption || discrR ].
 
302
  intros alp_f2d H11.
 
303
  assert (H12 := derivable_continuous_pt _ _ X).
 
304
  unfold continuity_pt in H12.
 
305
  unfold continue_in in H12.
 
306
  unfold limit1_in in H12.
 
307
  unfold limit_in in H12.
 
308
  unfold dist in H12.
 
309
  simpl in H12.
 
310
  unfold R_dist in H12.
 
311
  elim (H12 (Rabs (Rsqr (f2 x) * f2 x * eps / (8 * f1 x * l2)))).
 
312
  intros alp_f2c H13.
 
313
  cut (0 < Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d (Rmin alp_f2d alp_f2c))).
 
314
  intro.
 
315
  exists
 
316
    (mkposreal (Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d (Rmin alp_f2d alp_f2c)))
 
317
      H14).
 
318
  simpl in |- *; intros.
 
319
  assert (H17 := Rlt_le_trans _ _ _ H16 (Rmin_l _ _)).
 
320
  assert (H18 := Rlt_le_trans _ _ _ H16 (Rmin_r _ _)).
 
321
  assert (H19 := Rlt_le_trans _ _ _ H18 (Rmin_r _ _)).
 
322
  assert (H20 := Rlt_le_trans _ _ _ H19 (Rmin_l _ _)).
 
323
  assert (H21 := Rlt_le_trans _ _ _ H19 (Rmin_r _ _)).
 
324
  assert (H22 := Rlt_le_trans _ _ _ H18 (Rmin_l _ _)).
 
325
  assert (H23 := Rlt_le_trans _ _ _ H17 (Rmin_l _ _)).
 
326
  assert (H24 := Rlt_le_trans _ _ _ H17 (Rmin_r _ _)).
 
327
  clear H16 H17 H18 H19.
 
328
  cut
 
329
    (forall a:R,
 
330
      Rabs a < alp_f2c ->
 
331
      Rabs (f2 (x + a) - f2 x) <
 
332
      Rabs (Rsqr (f2 x) * f2 x * eps / (8 * f1 x * l2))).
 
333
  intro.
 
334
  rewrite formule; try assumption.
 
335
  apply Rle_lt_trans with
 
336
    (Rabs (/ f2 (x + h) * ((f1 (x + h) - f1 x) / h - l1)) +
 
337
      Rabs (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) +
 
338
      Rabs (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) +
 
339
      Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x))).
 
340
  unfold Rminus in |- *.
 
341
  rewrite <-
 
342
    (Rabs_Ropp (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) + - f2 x) / h + - l2)))
 
343
    .
 
344
  apply Rabs_4.
 
345
  repeat rewrite Rabs_mult.
 
346
  apply Rlt_le_trans with (eps / 4 + eps / 4 + eps / 4 + eps / 4).
 
347
  cut (Rabs (/ f2 (x + h)) * Rabs ((f1 (x + h) - f1 x) / h - l1) < eps / 4).
 
348
  cut (Rabs (l1 / (f2 x * f2 (x + h))) * Rabs (f2 x - f2 (x + h)) < eps / 4).
 
349
  cut
 
350
    (Rabs (f1 x / (f2 x * f2 (x + h))) * Rabs ((f2 (x + h) - f2 x) / h - l2) <
 
351
      eps / 4).
 
352
  cut
 
353
    (Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h))) * Rabs (f2 (x + h) - f2 x) <
 
354
      eps / 4).
 
355
  intros.
 
356
  apply Rlt_4; assumption.
 
357
  rewrite <- Rabs_mult.
 
358
  apply (maj_term4 x h eps l2 alp_f2 alp_f2c eps_f2 f1 f2); try assumption.
 
359
  apply H2; assumption.
 
360
  apply Rmin_2; assumption.
 
361
  rewrite <- Rabs_mult.
 
362
  apply (maj_term3 x h eps l2 alp_f2 eps_f2 alp_f2d f1 f2); try assumption.
 
363
  apply H2; assumption.
 
364
  apply Rmin_2; assumption.
 
365
  rewrite H9.
 
366
  unfold Rdiv in |- *; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
 
367
  rewrite Rabs_R0; rewrite Rmult_0_l.
 
368
  apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup ].
 
369
  rewrite <- Rabs_mult.
 
370
  apply (maj_term1 x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2); try assumption.
 
371
  apply H2; assumption.
 
372
  apply Rmin_2; assumption.
 
373
  right; symmetry  in |- *; apply quadruple_var.
 
374
  apply H2; assumption.
 
375
  intros.
 
376
  case (Req_dec a 0); intro.
 
377
  rewrite H17; rewrite Rplus_0_r.
 
378
  unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0.
 
379
  apply Rabs_pos_lt.
 
380
  unfold Rdiv, Rsqr in |- *.
 
381
  repeat rewrite Rinv_mult_distr; try assumption.
 
382
  repeat apply prod_neq_R0; try assumption.
 
383
  red in |- *; intro H18; rewrite H18 in H6; elim (Rlt_irrefl _ H6). 
 
384
  apply Rinv_neq_0_compat; discrR.
 
385
  apply Rinv_neq_0_compat; discrR.
 
386
  apply Rinv_neq_0_compat; discrR.
 
387
  apply Rinv_neq_0_compat; assumption.
 
388
  apply Rinv_neq_0_compat; assumption.
 
389
  discrR.
 
390
  discrR.
 
391
  discrR.
 
392
  discrR.
 
393
  discrR.
 
394
  apply prod_neq_R0; [ discrR | assumption ].
 
395
  elim H13; intros.
 
396
  apply H19.
 
397
  split.
 
398
  apply D_x_no_cond; assumption.
 
399
  replace (x + a - x) with a; [ assumption | ring ].
 
400
  repeat apply Rmin_pos.
 
401
  apply (cond_pos eps_f2).
 
402
  elim H3; intros; assumption.
 
403
  apply (cond_pos alp_f1d).
 
404
  apply (cond_pos alp_f2d).
 
405
  elim H13; intros; assumption.
 
406
  change (0 < Rabs (Rsqr (f2 x) * f2 x * eps / (8 * f1 x * l2))) in |- *.
 
407
  apply Rabs_pos_lt.
 
408
  unfold Rsqr, Rdiv in |- *.
 
409
  repeat rewrite Rinv_mult_distr; try assumption || discrR.
 
410
  repeat apply prod_neq_R0; try assumption.
 
411
  red in |- *; intro H13; rewrite H13 in H6; elim (Rlt_irrefl _ H6). 
 
412
  apply Rinv_neq_0_compat; discrR.
 
413
  apply Rinv_neq_0_compat; discrR.
 
414
  apply Rinv_neq_0_compat; discrR.
 
415
  apply Rinv_neq_0_compat; assumption.
 
416
  apply Rinv_neq_0_compat; assumption.
 
417
  apply prod_neq_R0; [ discrR | assumption ].
 
418
  red in |- *; intro H11; rewrite H11 in H6; elim (Rlt_irrefl _ H6). 
 
419
  apply Rinv_neq_0_compat; discrR.
 
420
  apply Rinv_neq_0_compat; discrR.
 
421
  apply Rinv_neq_0_compat; discrR.
 
422
  apply Rinv_neq_0_compat; assumption.
 
423
(***********************************)
 
424
(*              Cas n� 5           *)
 
425
(*    (f1 x)<>0  l1<>0  l2=0       *)
 
426
(***********************************)
 
427
  case (Req_dec l2 0); intro.
 
428
  assert (H11 := derivable_continuous_pt _ _ X).
 
429
  unfold continuity_pt in H11.
 
430
  unfold continue_in in H11.
 
431
  unfold limit1_in in H11.
 
432
  unfold limit_in in H11.
 
433
  unfold dist in H11.
 
434
  simpl in H11.
 
435
  unfold R_dist in H11.
 
436
  elim (H11 (Rabs (eps * Rsqr (f2 x) / (8 * l1)))).
 
437
  clear H11; intros alp_f2t2 H11.
 
438
  elim (H0 (Rabs (Rsqr (f2 x) * eps / (8 * f1 x)))).
 
439
  intros alp_f2d H12.
 
440
  cut (0 < Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d (Rmin alp_f2d alp_f2t2))).
 
441
  intro.
 
442
  exists
 
443
    (mkposreal
 
444
      (Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d (Rmin alp_f2d alp_f2t2))) H13).
 
445
  simpl in |- *.
 
446
  intros.
 
447
  cut
 
448
    (forall a:R,
 
449
      Rabs a < alp_f2t2 ->
 
450
      Rabs (f2 (x + a) - f2 x) < Rabs (eps * Rsqr (f2 x) / (8 * l1))).
 
451
  intro.
 
452
  assert (H17 := Rlt_le_trans _ _ _ H15 (Rmin_l _ _)).
 
453
  assert (H18 := Rlt_le_trans _ _ _ H15 (Rmin_r _ _)).
 
454
  assert (H19 := Rlt_le_trans _ _ _ H17 (Rmin_r _ _)).
 
455
  assert (H20 := Rlt_le_trans _ _ _ H17 (Rmin_l _ _)).
 
456
  assert (H21 := Rlt_le_trans _ _ _ H18 (Rmin_r _ _)).
 
457
  assert (H22 := Rlt_le_trans _ _ _ H18 (Rmin_l _ _)).
 
458
  assert (H23 := Rlt_le_trans _ _ _ H21 (Rmin_l _ _)).
 
459
  assert (H24 := Rlt_le_trans _ _ _ H21 (Rmin_r _ _)).
 
460
  clear H15 H17 H18 H21.
 
461
  rewrite formule; try assumption.
 
462
  apply Rle_lt_trans with
 
463
    (Rabs (/ f2 (x + h) * ((f1 (x + h) - f1 x) / h - l1)) +
 
464
      Rabs (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) +
 
465
      Rabs (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) +
 
466
      Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x))).
 
467
  unfold Rminus in |- *.
 
468
  rewrite <-
 
469
    (Rabs_Ropp (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) + - f2 x) / h + - l2)))
 
470
    .
 
471
  apply Rabs_4.
 
472
  repeat rewrite Rabs_mult.
 
473
  apply Rlt_le_trans with (eps / 4 + eps / 4 + eps / 4 + eps / 4).
 
474
  cut (Rabs (/ f2 (x + h)) * Rabs ((f1 (x + h) - f1 x) / h - l1) < eps / 4).
 
475
  cut (Rabs (l1 / (f2 x * f2 (x + h))) * Rabs (f2 x - f2 (x + h)) < eps / 4).
 
476
  cut
 
477
    (Rabs (f1 x / (f2 x * f2 (x + h))) * Rabs ((f2 (x + h) - f2 x) / h - l2) <
 
478
      eps / 4).
 
479
  cut
 
480
    (Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h))) * Rabs (f2 (x + h) - f2 x) <
 
481
      eps / 4).
 
482
  intros.
 
483
  apply Rlt_4; assumption.
 
484
  rewrite H10.
 
485
  unfold Rdiv in |- *; repeat rewrite Rmult_0_r || rewrite Rmult_0_l.
 
486
  rewrite Rabs_R0; rewrite Rmult_0_l.
 
487
  apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup ].
 
488
  rewrite <- Rabs_mult.
 
489
  apply (maj_term3 x h eps l2 alp_f2 eps_f2 alp_f2d f1 f2); try assumption.
 
490
  apply H2; assumption.
 
491
  apply Rmin_2; assumption.
 
492
  rewrite <- Rabs_mult.
 
493
  apply (maj_term2 x h eps l1 alp_f2 alp_f2t2 eps_f2 f2); try assumption.
 
494
  apply H2; assumption.
 
495
  apply Rmin_2; assumption.
 
496
  rewrite <- Rabs_mult.
 
497
  apply (maj_term1 x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2); try assumption.
 
498
  apply H2; assumption.
 
499
  apply Rmin_2; assumption.
 
500
  right; symmetry  in |- *; apply quadruple_var.
 
501
  apply H2; assumption.
 
502
  intros.
 
503
  case (Req_dec a 0); intro.
 
504
  rewrite H17; rewrite Rplus_0_r; unfold Rminus in |- *; rewrite Rplus_opp_r;
 
505
    rewrite Rabs_R0.
 
506
  apply Rabs_pos_lt.
 
507
  unfold Rdiv in |- *; rewrite Rinv_mult_distr; try discrR || assumption.
 
508
  unfold Rsqr in |- *.
 
509
  repeat apply prod_neq_R0;
 
510
    assumption ||
 
511
      (apply Rinv_neq_0_compat; assumption) ||
 
512
        (apply Rinv_neq_0_compat; discrR) ||
 
513
          (red in |- *; intro H18; rewrite H18 in H6; elim (Rlt_irrefl _ H6)).
 
514
  elim H11; intros.
 
515
  apply H19.
 
516
  split.
 
517
  apply D_x_no_cond; assumption.
 
518
  replace (x + a - x) with a; [ assumption | ring ].
 
519
  repeat apply Rmin_pos.
 
520
  apply (cond_pos eps_f2).
 
521
  elim H3; intros; assumption.
 
522
  apply (cond_pos alp_f1d). 
 
523
  apply (cond_pos alp_f2d).
 
524
  elim H11; intros; assumption.
 
525
  apply Rabs_pos_lt.
 
526
  unfold Rdiv, Rsqr in |- *; rewrite Rinv_mult_distr; try discrR || assumption.
 
527
  repeat apply prod_neq_R0;
 
528
    assumption ||
 
529
      (apply Rinv_neq_0_compat; assumption) ||
 
530
        (apply Rinv_neq_0_compat; discrR) ||
 
531
          (red in |- *; intro H12; rewrite H12 in H6; elim (Rlt_irrefl _ H6)).
 
532
  change (0 < Rabs (eps * Rsqr (f2 x) / (8 * l1))) in |- *.
 
533
  apply Rabs_pos_lt.
 
534
  unfold Rdiv, Rsqr in |- *; rewrite Rinv_mult_distr; try discrR || assumption.
 
535
  repeat apply prod_neq_R0;
 
536
    assumption ||
 
537
      (apply Rinv_neq_0_compat; assumption) ||
 
538
        (apply Rinv_neq_0_compat; discrR) ||
 
539
          (red in |- *; intro H12; rewrite H12 in H6; elim (Rlt_irrefl _ H6)).
 
540
(***********************************)
 
541
(*              Cas n� 6           *)
 
542
(*    (f1 x)<>0  l1<>0  l2<>0      *)
 
543
(***********************************)
 
544
  elim (H0 (Rabs (Rsqr (f2 x) * eps / (8 * f1 x)))).
 
545
  intros alp_f2d H11.
 
546
  assert (H12 := derivable_continuous_pt _ _ X).
 
547
  unfold continuity_pt in H12.
 
548
  unfold continue_in in H12.
 
549
  unfold limit1_in in H12.
 
550
  unfold limit_in in H12.
 
551
  unfold dist in H12.
 
552
  simpl in H12.
 
553
  unfold R_dist in H12.
 
554
  elim (H12 (Rabs (Rsqr (f2 x) * f2 x * eps / (8 * f1 x * l2)))).
 
555
  intros alp_f2c H13.
 
556
  elim (H12 (Rabs (eps * Rsqr (f2 x) / (8 * l1)))).
 
557
  intros alp_f2t2 H14.
 
558
  cut
 
559
    (0 <
 
560
      Rmin (Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d alp_f2d))
 
561
      (Rmin alp_f2c alp_f2t2)).
 
562
  intro.
 
563
  exists
 
564
    (mkposreal
 
565
      (Rmin (Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d alp_f2d))
 
566
        (Rmin alp_f2c alp_f2t2)) H15).
 
567
  simpl in |- *.
 
568
  intros.
 
569
  assert (H18 := Rlt_le_trans _ _ _ H17 (Rmin_l _ _)).
 
570
  assert (H19 := Rlt_le_trans _ _ _ H17 (Rmin_r _ _)).
 
571
  assert (H20 := Rlt_le_trans _ _ _ H18 (Rmin_l _ _)).
 
572
  assert (H21 := Rlt_le_trans _ _ _ H18 (Rmin_r _ _)).
 
573
  assert (H22 := Rlt_le_trans _ _ _ H19 (Rmin_l _ _)).
 
574
  assert (H23 := Rlt_le_trans _ _ _ H19 (Rmin_r _ _)).
 
575
  assert (H24 := Rlt_le_trans _ _ _ H20 (Rmin_l _ _)).
 
576
  assert (H25 := Rlt_le_trans _ _ _ H20 (Rmin_r _ _)).
 
577
  assert (H26 := Rlt_le_trans _ _ _ H21 (Rmin_l _ _)).
 
578
  assert (H27 := Rlt_le_trans _ _ _ H21 (Rmin_r _ _)).
 
579
  clear H17 H18 H19 H20 H21.
 
580
  cut
 
581
    (forall a:R,
 
582
      Rabs a < alp_f2t2 ->
 
583
      Rabs (f2 (x + a) - f2 x) < Rabs (eps * Rsqr (f2 x) / (8 * l1))).
 
584
  cut
 
585
    (forall a:R,
 
586
      Rabs a < alp_f2c ->
 
587
      Rabs (f2 (x + a) - f2 x) <
 
588
      Rabs (Rsqr (f2 x) * f2 x * eps / (8 * f1 x * l2))).
 
589
  intros.
 
590
  rewrite formule; try assumption.
 
591
  apply Rle_lt_trans with
 
592
    (Rabs (/ f2 (x + h) * ((f1 (x + h) - f1 x) / h - l1)) +
 
593
      Rabs (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) +
 
594
      Rabs (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) +
 
595
      Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x))).
 
596
  unfold Rminus in |- *.
 
597
  rewrite <-
 
598
    (Rabs_Ropp (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) + - f2 x) / h + - l2)))
 
599
    .
 
600
  apply Rabs_4.
 
601
  repeat rewrite Rabs_mult.
 
602
  apply Rlt_le_trans with (eps / 4 + eps / 4 + eps / 4 + eps / 4).
 
603
  cut (Rabs (/ f2 (x + h)) * Rabs ((f1 (x + h) - f1 x) / h - l1) < eps / 4).
 
604
  cut (Rabs (l1 / (f2 x * f2 (x + h))) * Rabs (f2 x - f2 (x + h)) < eps / 4).
 
605
  cut
 
606
    (Rabs (f1 x / (f2 x * f2 (x + h))) * Rabs ((f2 (x + h) - f2 x) / h - l2) <
 
607
      eps / 4).
 
608
  cut
 
609
    (Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h))) * Rabs (f2 (x + h) - f2 x) <
 
610
      eps / 4).
 
611
  intros.
 
612
  apply Rlt_4; assumption.
 
613
  rewrite <- Rabs_mult.
 
614
  apply (maj_term4 x h eps l2 alp_f2 alp_f2c eps_f2 f1 f2); try assumption.
 
615
  apply H2; assumption.
 
616
  apply Rmin_2; assumption.
 
617
  rewrite <- Rabs_mult.
 
618
  apply (maj_term3 x h eps l2 alp_f2 eps_f2 alp_f2d f1 f2); try assumption.
 
619
  apply H2; assumption.
 
620
  apply Rmin_2; assumption.
 
621
  rewrite <- Rabs_mult.
 
622
  apply (maj_term2 x h eps l1 alp_f2 alp_f2t2 eps_f2 f2); try assumption.
 
623
  apply H2; assumption.
 
624
  apply Rmin_2; assumption.
 
625
  rewrite <- Rabs_mult.
 
626
  apply (maj_term1 x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2); try assumption.
 
627
  apply H2; assumption.
 
628
  apply Rmin_2; assumption.
 
629
  right; symmetry  in |- *; apply quadruple_var.
 
630
  apply H2; assumption.
 
631
  intros.
 
632
  case (Req_dec a 0); intro.
 
633
  rewrite H18; rewrite Rplus_0_r; unfold Rminus in |- *; rewrite Rplus_opp_r;
 
634
    rewrite Rabs_R0; apply Rabs_pos_lt.
 
635
  unfold Rdiv, Rsqr in |- *; rewrite Rinv_mult_distr.
 
636
  repeat apply prod_neq_R0;
 
637
    assumption ||
 
638
      (apply Rinv_neq_0_compat; assumption) ||
 
639
        (apply Rinv_neq_0_compat; discrR) ||
 
640
          (red in |- *; intro H28; rewrite H28 in H6; elim (Rlt_irrefl _ H6)).
 
641
  apply prod_neq_R0; [ discrR | assumption ].
 
642
  apply prod_neq_R0; [ discrR | assumption ].
 
643
  assumption.
 
644
  elim H13; intros.
 
645
  apply H20.
 
646
  split.
 
647
  apply D_x_no_cond; assumption.
 
648
  replace (x + a - x) with a; [ assumption | ring ].
 
649
  intros.
 
650
  case (Req_dec a 0); intro.
 
651
  rewrite H18; rewrite Rplus_0_r; unfold Rminus in |- *; rewrite Rplus_opp_r;
 
652
    rewrite Rabs_R0; apply Rabs_pos_lt.
 
653
  unfold Rdiv, Rsqr in |- *; rewrite Rinv_mult_distr.
 
654
  repeat apply prod_neq_R0;
 
655
    assumption ||
 
656
      (apply Rinv_neq_0_compat; assumption) ||
 
657
        (apply Rinv_neq_0_compat; discrR) ||
 
658
          (red in |- *; intro H28; rewrite H28 in H6; elim (Rlt_irrefl _ H6)).
 
659
  discrR.
 
660
  assumption.
 
661
  elim H14; intros.
 
662
  apply H20.
 
663
  split.
 
664
  unfold D_x, no_cond in |- *; split.
 
665
  trivial.
 
666
  apply Rminus_not_eq_right.
 
667
  replace (x + a - x) with a; [ assumption | ring ].
 
668
  replace (x + a - x) with a; [ assumption | ring ].
 
669
  repeat apply Rmin_pos.
 
670
  apply (cond_pos eps_f2).
 
671
  elim H3; intros; assumption.
 
672
  apply (cond_pos alp_f1d).
 
673
  apply (cond_pos alp_f2d).
 
674
  elim H13; intros; assumption.
 
675
  elim H14; intros; assumption.
 
676
  change (0 < Rabs (eps * Rsqr (f2 x) / (8 * l1))) in |- *; apply Rabs_pos_lt.
 
677
  unfold Rdiv, Rsqr in |- *; rewrite Rinv_mult_distr; try discrR || assumption.
 
678
  repeat apply prod_neq_R0;
 
679
    assumption ||
 
680
      (apply Rinv_neq_0_compat; assumption) ||
 
681
        (apply Rinv_neq_0_compat; discrR) ||
 
682
          (red in |- *; intro H14; rewrite H14 in H6; elim (Rlt_irrefl _ H6)).
 
683
  change (0 < Rabs (Rsqr (f2 x) * f2 x * eps / (8 * f1 x * l2))) in |- *;
 
684
    apply Rabs_pos_lt.
 
685
  unfold Rdiv, Rsqr in |- *; rewrite Rinv_mult_distr.
 
686
  repeat apply prod_neq_R0;
 
687
    assumption ||
 
688
      (apply Rinv_neq_0_compat; assumption) ||
 
689
        (apply Rinv_neq_0_compat; discrR) ||
 
690
          (red in |- *; intro H13; rewrite H13 in H6; elim (Rlt_irrefl _ H6)).
 
691
  apply prod_neq_R0; [ discrR | assumption ].
 
692
  apply prod_neq_R0; [ discrR | assumption ].
 
693
  assumption.
 
694
  apply Rabs_pos_lt.
 
695
  unfold Rdiv, Rsqr in |- *; rewrite Rinv_mult_distr;
 
696
    [ idtac | discrR | assumption ].
 
697
  repeat apply prod_neq_R0;
 
698
    assumption ||
 
699
      (apply Rinv_neq_0_compat; assumption) ||
 
700
        (apply Rinv_neq_0_compat; discrR) ||
 
701
          (red in |- *; intro H11; rewrite H11 in H6; elim (Rlt_irrefl _ H6)).
 
702
  intros.
 
703
  unfold Rdiv in |- *.
 
704
  apply Rmult_lt_reg_l with (Rabs (f2 (x + a))).
 
705
  apply Rabs_pos_lt; apply H2.
 
706
  apply Rlt_le_trans with (Rmin eps_f2 alp_f2).
 
707
  assumption.
 
708
  apply Rmin_l.
 
709
  rewrite <- Rinv_r_sym.
 
710
  apply Rmult_lt_reg_l with (Rabs (f2 x)).
 
711
  apply Rabs_pos_lt; assumption.
 
712
  rewrite Rmult_1_r.
 
713
  rewrite (Rmult_comm (Rabs (f2 x))).
 
714
  repeat rewrite Rmult_assoc.
 
715
  rewrite <- Rinv_l_sym.
 
716
  rewrite Rmult_1_r.
 
717
  apply Rmult_lt_reg_l with (/ 2).
 
718
  apply Rinv_0_lt_compat; prove_sup0.
 
719
  repeat rewrite (Rmult_comm (/ 2)).
 
720
  repeat rewrite Rmult_assoc.
 
721
  rewrite <- Rinv_r_sym.
 
722
  rewrite Rmult_1_r.
 
723
  unfold Rdiv in H5; apply H5.
 
724
  replace (x + a - x) with a.
 
725
  assert (H7 := Rlt_le_trans _ _ _ H6 (Rmin_r _ _)); assumption.
 
726
  ring.
 
727
  discrR.
 
728
  apply Rabs_no_R0; assumption.
 
729
  apply Rabs_no_R0; apply H2.
 
730
  assert (H7 := Rlt_le_trans _ _ _ H6 (Rmin_l _ _)); assumption.
 
731
  intros.
 
732
  assert (H6 := H4 a H5).
 
733
  rewrite <- (Rabs_Ropp (f2 a - f2 x)) in H6.
 
734
  rewrite Ropp_minus_distr in H6.
 
735
  assert (H7 := Rle_lt_trans _ _ _ (Rabs_triang_inv _ _) H6).
 
736
  apply Rplus_lt_reg_r with (- Rabs (f2 a) + Rabs (f2 x) / 2).
 
737
  rewrite Rplus_assoc.
 
738
  rewrite <- double_var.
 
739
  do 2 rewrite (Rplus_comm (- Rabs (f2 a))).
 
740
  rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r.
 
741
  unfold Rminus in H7; assumption.
 
742
  intros.
 
743
  case (Req_dec x x0); intro.
 
744
  rewrite <- H5; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0;
 
745
    unfold Rdiv in |- *; apply Rmult_lt_0_compat;
 
746
      [ apply Rabs_pos_lt; assumption | apply Rinv_0_lt_compat; prove_sup0 ].
 
747
  elim H3; intros.
 
748
  apply H7.
 
749
  split.
 
750
  unfold D_x, no_cond in |- *; split.
 
751
  trivial.
 
752
  assumption.
 
753
  assumption.
 
754
Qed.
 
755
 
 
756
Lemma derivable_pt_div :
 
757
  forall (f1 f2:R -> R) (x:R),
 
758
    derivable_pt f1 x ->
 
759
    derivable_pt f2 x -> f2 x <> 0 -> derivable_pt (f1 / f2) x.
 
760
Proof.
 
761
  unfold derivable_pt in |- *.
 
762
  intros f1 f2 x X X0 H.
 
763
  elim X; intros.
 
764
  elim X0; intros.
 
765
  exists ((x0 * f2 x - x1 * f1 x) / Rsqr (f2 x)).
 
766
  apply derivable_pt_lim_div; assumption.
 
767
Qed.
 
768
 
 
769
Lemma derivable_div :
 
770
  forall f1 f2:R -> R,
 
771
    derivable f1 ->
 
772
    derivable f2 -> (forall x:R, f2 x <> 0) -> derivable (f1 / f2).
 
773
Proof.
 
774
  unfold derivable in |- *; intros f1 f2 X X0 H x.
 
775
  apply (derivable_pt_div _ _ _ (X x) (X0 x) (H x)).
 
776
Qed.
 
777
 
 
778
Lemma derive_pt_div :
 
779
  forall (f1 f2:R -> R) (x:R) (pr1:derivable_pt f1 x) 
 
780
    (pr2:derivable_pt f2 x) (na:f2 x <> 0),
 
781
    derive_pt (f1 / f2) x (derivable_pt_div _ _ _ pr1 pr2 na) =
 
782
    (derive_pt f1 x pr1 * f2 x - derive_pt f2 x pr2 * f1 x) / Rsqr (f2 x).
 
783
Proof.
 
784
  intros.
 
785
  assert (H := derivable_derive f1 x pr1).
 
786
  assert (H0 := derivable_derive f2 x pr2).
 
787
  assert
 
788
    (H1 := derivable_derive (f1 / f2)%F x (derivable_pt_div _ _ _ pr1 pr2 na)).
 
789
  elim H; clear H; intros l1 H.
 
790
  elim H0; clear H0; intros l2 H0.
 
791
  elim H1; clear H1; intros l H1.
 
792
  rewrite H; rewrite H0; apply derive_pt_eq_0.
 
793
  assert (H3 := proj2_sig pr1).
 
794
  unfold derive_pt in H; rewrite H in H3.
 
795
  assert (H4 := proj2_sig pr2).
 
796
  unfold derive_pt in H0; rewrite H0 in H4.
 
797
  apply derivable_pt_lim_div; assumption.
 
798
Qed.