← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/Reals/R_sqrt.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/R_sqrt.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: R_sqrt.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
10
 
 
11
Require Import Rbase.
 
12
Require Import Rfunctions.
 
13
Require Import Rsqrt_def.
 
14
Open Local Scope R_scope.
 
15
 
 
16
(** * Continuous extension of Rsqrt on R *)
 
17
Definition sqrt (x:R) : R :=
 
18
  match Rcase_abs x with
 
19
    | left _ => 0
 
20
    | right a => Rsqrt (mknonnegreal x (Rge_le _ _ a))
 
21
  end.
 
22
 
 
23
Lemma sqrt_positivity : forall x:R, 0 <= x -> 0 <= sqrt x.
 
24
Proof.
 
25
  intros.
 
26
  unfold sqrt in |- *.
 
27
  case (Rcase_abs x); intro.
 
28
  elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ r H)).
 
29
  apply Rsqrt_positivity.
 
30
Qed.
 
31
 
 
32
Lemma sqrt_sqrt : forall x:R, 0 <= x -> sqrt x * sqrt x = x.
 
33
Proof.
 
34
  intros.
 
35
  unfold sqrt in |- *.
 
36
  case (Rcase_abs x); intro.
 
37
  elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ r H)).
 
38
  rewrite Rsqrt_Rsqrt; reflexivity.
 
39
Qed.
 
40
 
 
41
Lemma sqrt_0 : sqrt 0 = 0.
 
42
Proof.
 
43
  apply Rsqr_eq_0; unfold Rsqr in |- *; apply sqrt_sqrt; right; reflexivity. 
 
44
Qed.
 
45
 
 
46
Lemma sqrt_1 : sqrt 1 = 1.
 
47
Proof.
 
48
  apply (Rsqr_inj (sqrt 1) 1);
 
49
    [ apply sqrt_positivity; left
 
50
      | left
 
51
      | unfold Rsqr in |- *; rewrite sqrt_sqrt; [ ring | left ] ]; 
 
52
    apply Rlt_0_1.
 
53
Qed.
 
54
 
 
55
Lemma sqrt_eq_0 : forall x:R, 0 <= x -> sqrt x = 0 -> x = 0.
 
56
Proof.
 
57
  intros; cut (Rsqr (sqrt x) = 0).
 
58
  intro; unfold Rsqr in H1; rewrite sqrt_sqrt in H1; assumption.
 
59
  rewrite H0; apply Rsqr_0.
 
60
Qed.
 
61
 
 
62
Lemma sqrt_lem_0 : forall x y:R, 0 <= x -> 0 <= y -> sqrt x = y -> y * y = x.
 
63
Proof.
 
64
  intros; rewrite <- H1; apply (sqrt_sqrt x H).
 
65
Qed.
 
66
 
 
67
Lemma sqrt_lem_1 : forall x y:R, 0 <= x -> 0 <= y -> y * y = x -> sqrt x = y.
 
68
Proof.
 
69
  intros; apply Rsqr_inj;
 
70
    [ apply (sqrt_positivity x H)
 
71
      | assumption
 
72
      | unfold Rsqr in |- *; rewrite H1; apply (sqrt_sqrt x H) ].
 
73
Qed.
 
74
 
 
75
Lemma sqrt_def : forall x:R, 0 <= x -> sqrt x * sqrt x = x.
 
76
Proof.
 
77
  intros; apply (sqrt_sqrt x H).
 
78
Qed.
 
79
 
 
80
Lemma sqrt_square : forall x:R, 0 <= x -> sqrt (x * x) = x.
 
81
Proof.
 
82
  intros;
 
83
    apply
 
84
      (Rsqr_inj (sqrt (Rsqr x)) x (sqrt_positivity (Rsqr x) (Rle_0_sqr x)) H);
 
85
      unfold Rsqr in |- *; apply (sqrt_sqrt (Rsqr x) (Rle_0_sqr x)).
 
86
Qed.
 
87
 
 
88
Lemma sqrt_Rsqr : forall x:R, 0 <= x -> sqrt (Rsqr x) = x.
 
89
Proof.
 
90
  intros; unfold Rsqr in |- *; apply sqrt_square; assumption.
 
91
Qed.
 
92
 
 
93
Lemma sqrt_Rsqr_abs : forall x:R, sqrt (Rsqr x) = Rabs x.
 
94
Proof.
 
95
  intro x; rewrite Rsqr_abs; apply sqrt_Rsqr; apply Rabs_pos.
 
96
Qed.
 
97
 
 
98
Lemma Rsqr_sqrt : forall x:R, 0 <= x -> Rsqr (sqrt x) = x.
 
99
Proof.
 
100
  intros x H1; unfold Rsqr in |- *; apply (sqrt_sqrt x H1).
 
101
Qed.
 
102
 
 
103
Lemma sqrt_mult :
 
104
  forall x y:R, 0 <= x -> 0 <= y -> sqrt (x * y) = sqrt x * sqrt y.
 
105
Proof.
 
106
  intros x y H1 H2;
 
107
    apply
 
108
      (Rsqr_inj (sqrt (x * y)) (sqrt x * sqrt y)
 
109
        (sqrt_positivity (x * y) (Rmult_le_pos x y H1 H2))
 
110
        (Rmult_le_pos (sqrt x) (sqrt y) (sqrt_positivity x H1)
 
111
          (sqrt_positivity y H2))); rewrite Rsqr_mult; 
 
112
      repeat rewrite Rsqr_sqrt;
 
113
        [ ring | assumption | assumption | apply (Rmult_le_pos x y H1 H2) ].
 
114
Qed.
 
115
 
 
116
Lemma sqrt_lt_R0 : forall x:R, 0 < x -> 0 < sqrt x.
 
117
Proof.
 
118
  intros x H1; apply Rsqr_incrst_0;
 
119
    [ rewrite Rsqr_0; rewrite Rsqr_sqrt; [ assumption | left; assumption ]
 
120
      | right; reflexivity
 
121
      | apply (sqrt_positivity x (Rlt_le 0 x H1)) ].
 
122
Qed.
 
123
 
 
124
Lemma sqrt_div :
 
125
  forall x y:R, 0 <= x -> 0 < y -> sqrt (x / y) = sqrt x / sqrt y.
 
126
Proof.
 
127
  intros x y H1 H2; apply Rsqr_inj;
 
128
    [ apply sqrt_positivity; apply (Rmult_le_pos x (/ y));
 
129
      [ assumption
 
130
        | generalize (Rinv_0_lt_compat y H2); clear H2; intro H2; left;
 
131
          assumption ]
 
132
      | apply (Rmult_le_pos (sqrt x) (/ sqrt y));
 
133
        [ apply (sqrt_positivity x H1)
 
134
          | generalize (sqrt_lt_R0 y H2); clear H2; intro H2;
 
135
            generalize (Rinv_0_lt_compat (sqrt y) H2); clear H2; 
 
136
              intro H2; left; assumption ]
 
137
      | rewrite Rsqr_div; repeat rewrite Rsqr_sqrt;
 
138
        [ reflexivity
 
139
          | left; assumption
 
140
          | assumption
 
141
          | generalize (Rinv_0_lt_compat y H2); intro H3;
 
142
            generalize (Rlt_le 0 (/ y) H3); intro H4;
 
143
              apply (Rmult_le_pos x (/ y) H1 H4)
 
144
          | red in |- *; intro H3; generalize (Rlt_le 0 y H2); intro H4;
 
145
            generalize (sqrt_eq_0 y H4 H3); intro H5; rewrite H5 in H2;
 
146
              elim (Rlt_irrefl 0 H2) ] ].
 
147
Qed.
 
148
 
 
149
Lemma sqrt_lt_0 : forall x y:R, 0 <= x -> 0 <= y -> sqrt x < sqrt y -> x < y.
 
150
Proof.
 
151
  intros x y H1 H2 H3;
 
152
    generalize
 
153
      (Rsqr_incrst_1 (sqrt x) (sqrt y) H3 (sqrt_positivity x H1)
 
154
        (sqrt_positivity y H2)); intro H4; rewrite (Rsqr_sqrt x H1) in H4;
 
155
      rewrite (Rsqr_sqrt y H2) in H4; assumption.
 
156
Qed.
 
157
 
 
158
Lemma sqrt_lt_1 : forall x y:R, 0 <= x -> 0 <= y -> x < y -> sqrt x < sqrt y.
 
159
Proof.
 
160
  intros x y H1 H2 H3; apply Rsqr_incrst_0;
 
161
    [ rewrite (Rsqr_sqrt x H1); rewrite (Rsqr_sqrt y H2); assumption
 
162
      | apply (sqrt_positivity x H1)
 
163
      | apply (sqrt_positivity y H2) ].
 
164
Qed.
 
165
 
 
166
Lemma sqrt_le_0 :
 
167
  forall x y:R, 0 <= x -> 0 <= y -> sqrt x <= sqrt y -> x <= y.
 
168
Proof.
 
169
  intros x y H1 H2 H3;
 
170
    generalize
 
171
      (Rsqr_incr_1 (sqrt x) (sqrt y) H3 (sqrt_positivity x H1)
 
172
        (sqrt_positivity y H2)); intro H4; rewrite (Rsqr_sqrt x H1) in H4;
 
173
      rewrite (Rsqr_sqrt y H2) in H4; assumption.
 
174
Qed.
 
175
 
 
176
Lemma sqrt_le_1 :
 
177
  forall x y:R, 0 <= x -> 0 <= y -> x <= y -> sqrt x <= sqrt y.
 
178
Proof.
 
179
  intros x y H1 H2 H3; apply Rsqr_incr_0;
 
180
    [ rewrite (Rsqr_sqrt x H1); rewrite (Rsqr_sqrt y H2); assumption
 
181
      | apply (sqrt_positivity x H1)
 
182
      | apply (sqrt_positivity y H2) ].
 
183
Qed.
 
184
 
 
185
Lemma sqrt_inj : forall x y:R, 0 <= x -> 0 <= y -> sqrt x = sqrt y -> x = y.
 
186
Proof.
 
187
  intros; cut (Rsqr (sqrt x) = Rsqr (sqrt y)).
 
188
  intro; rewrite (Rsqr_sqrt x H) in H2; rewrite (Rsqr_sqrt y H0) in H2;
 
189
    assumption.
 
190
  rewrite H1; reflexivity.
 
191
Qed.
 
192
 
 
193
Lemma sqrt_less : forall x:R, 0 <= x -> 1 < x -> sqrt x < x.
 
194
Proof.
 
195
  intros x H1 H2; generalize (sqrt_lt_1 1 x (Rlt_le 0 1 Rlt_0_1) H1 H2);
 
196
    intro H3; rewrite sqrt_1 in H3; generalize (Rmult_ne (sqrt x)); 
 
197
      intro H4; elim H4; intros H5 H6; rewrite <- H5; pattern x at 2 in |- *;
 
198
        rewrite <- (sqrt_def x H1);
 
199
          apply
 
200
            (Rmult_lt_compat_l (sqrt x) 1 (sqrt x)
 
201
              (sqrt_lt_R0 x (Rlt_trans 0 1 x Rlt_0_1 H2)) H3).
 
202
Qed.
 
203
 
 
204
Lemma sqrt_more : forall x:R, 0 < x -> x < 1 -> x < sqrt x.
 
205
Proof.
 
206
  intros x H1 H2;
 
207
    generalize (sqrt_lt_1 x 1 (Rlt_le 0 x H1) (Rlt_le 0 1 Rlt_0_1) H2); 
 
208
      intro H3; rewrite sqrt_1 in H3; generalize (Rmult_ne (sqrt x)); 
 
209
        intro H4; elim H4; intros H5 H6; rewrite <- H5; pattern x at 1 in |- *;
 
210
          rewrite <- (sqrt_def x (Rlt_le 0 x H1));
 
211
            apply (Rmult_lt_compat_l (sqrt x) (sqrt x) 1 (sqrt_lt_R0 x H1) H3).
 
212
Qed.
 
213
 
 
214
Lemma sqrt_cauchy :
 
215
  forall a b c d:R,
 
216
    a * c + b * d <= sqrt (Rsqr a + Rsqr b) * sqrt (Rsqr c + Rsqr d).
 
217
Proof.
 
218
  intros a b c d; apply Rsqr_incr_0_var;
 
219
    [ rewrite Rsqr_mult; repeat rewrite Rsqr_sqrt; unfold Rsqr in |- *;
 
220
      [ replace ((a * c + b * d) * (a * c + b * d)) with
 
221
        (a * a * c * c + b * b * d * d + 2 * a * b * c * d);
 
222
        [ replace ((a * a + b * b) * (c * c + d * d)) with
 
223
          (a * a * c * c + b * b * d * d + (a * a * d * d + b * b * c * c));
 
224
          [ apply Rplus_le_compat_l;
 
225
            replace (a * a * d * d + b * b * c * c) with
 
226
            (2 * a * b * c * d +
 
227
              (a * a * d * d + b * b * c * c - 2 * a * b * c * d));
 
228
            [ pattern (2 * a * b * c * d) at 1 in |- *; rewrite <- Rplus_0_r;
 
229
              apply Rplus_le_compat_l;
 
230
                replace (a * a * d * d + b * b * c * c - 2 * a * b * c * d)
 
231
              with (Rsqr (a * d - b * c));
 
232
                [ apply Rle_0_sqr | unfold Rsqr in |- *; ring ]
 
233
              | ring ]
 
234
            | ring ]
 
235
          | ring ]
 
236
        | apply
 
237
          (Rplus_le_le_0_compat (Rsqr c) (Rsqr d) (Rle_0_sqr c) (Rle_0_sqr d))
 
238
        | apply
 
239
          (Rplus_le_le_0_compat (Rsqr a) (Rsqr b) (Rle_0_sqr a) (Rle_0_sqr b)) ]
 
240
      | apply Rmult_le_pos; apply sqrt_positivity; apply Rplus_le_le_0_compat;
 
241
        apply Rle_0_sqr ].
 
242
Qed.
 
243
 
 
244
(************************************************************)
 
245
(** * Resolution of [a*X^2+b*X+c=0]                         *)
 
246
(************************************************************)
 
247
 
 
248
Definition Delta (a:nonzeroreal) (b c:R) : R := Rsqr b - 4 * a * c.
 
249
 
 
250
Definition Delta_is_pos (a:nonzeroreal) (b c:R) : Prop := 0 <= Delta a b c.
 
251
 
 
252
Definition sol_x1 (a:nonzeroreal) (b c:R) : R :=
 
253
  (- b + sqrt (Delta a b c)) / (2 * a).
 
254
 
 
255
Definition sol_x2 (a:nonzeroreal) (b c:R) : R :=
 
256
  (- b - sqrt (Delta a b c)) / (2 * a).
 
257
 
 
258
Lemma Rsqr_sol_eq_0_1 :
 
259
  forall (a:nonzeroreal) (b c x:R),
 
260
    Delta_is_pos a b c ->
 
261
    x = sol_x1 a b c \/ x = sol_x2 a b c -> a * Rsqr x + b * x + c = 0.
 
262
Proof.
 
263
  intros; elim H0; intro.
 
264
  unfold sol_x1 in H1; unfold Delta in H1; rewrite H1; unfold Rdiv in |- *;
 
265
    repeat rewrite Rsqr_mult; rewrite Rsqr_plus; rewrite <- Rsqr_neg;
 
266
      rewrite Rsqr_sqrt.
 
267
  rewrite Rsqr_inv.
 
268
  unfold Rsqr in |- *; repeat rewrite Rinv_mult_distr.
 
269
  repeat rewrite Rmult_assoc; rewrite (Rmult_comm a).
 
270
  repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
 
271
  rewrite Rmult_1_r; rewrite Rmult_plus_distr_r.
 
272
  repeat rewrite Rmult_assoc.
 
273
  pattern 2 at 2 in |- *; rewrite (Rmult_comm 2).
 
274
  repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
 
275
  rewrite Rmult_1_r.
 
276
  rewrite
 
277
    (Rmult_plus_distr_r (- b) (sqrt (b * b - 2 * (2 * (a * c)))) (/ 2 * / a))
 
278
    .
 
279
  rewrite Rmult_plus_distr_l; repeat rewrite Rplus_assoc.
 
280
  replace
 
281
  (- b * (sqrt (b * b - 2 * (2 * (a * c))) * (/ 2 * / a)) +
 
282
    (b * (- b * (/ 2 * / a)) +
 
283
      (b * (sqrt (b * b - 2 * (2 * (a * c))) * (/ 2 * / a)) + c))) with
 
284
  (b * (- b * (/ 2 * / a)) + c).
 
285
  unfold Rminus in |- *; repeat rewrite <- Rplus_assoc.
 
286
  replace (b * b + b * b) with (2 * (b * b)).
 
287
  rewrite Rmult_plus_distr_r; repeat rewrite Rmult_assoc.
 
288
  rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc.
 
289
  rewrite <- Rinv_l_sym.
 
290
  rewrite Rmult_1_r.
 
291
  rewrite Ropp_mult_distr_l_reverse; repeat rewrite Rmult_assoc;
 
292
    rewrite (Rmult_comm 2).
 
293
  repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
 
294
  rewrite Rmult_1_r; rewrite (Rmult_comm (/ 2)); repeat rewrite Rmult_assoc;
 
295
    rewrite (Rmult_comm 2).
 
296
  repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
 
297
  rewrite Rmult_1_r; repeat rewrite Rmult_assoc.
 
298
  rewrite (Rmult_comm a); rewrite Rmult_assoc.
 
299
  rewrite <- Rinv_l_sym.
 
300
  rewrite Rmult_1_r; rewrite <- Rmult_opp_opp.
 
301
  ring.
 
302
  apply (cond_nonzero a).
 
303
  discrR.
 
304
  discrR.
 
305
  discrR.
 
306
  ring.
 
307
  ring.
 
308
  discrR.
 
309
  apply (cond_nonzero a).
 
310
  discrR.
 
311
  apply (cond_nonzero a).
 
312
  apply prod_neq_R0; [ discrR | apply (cond_nonzero a) ].
 
313
  apply prod_neq_R0; [ discrR | apply (cond_nonzero a) ].
 
314
  apply prod_neq_R0; [ discrR | apply (cond_nonzero a) ].
 
315
  assumption.
 
316
  unfold sol_x2 in H1; unfold Delta in H1; rewrite H1; unfold Rdiv in |- *;
 
317
    repeat rewrite Rsqr_mult; rewrite Rsqr_minus; rewrite <- Rsqr_neg;
 
318
      rewrite Rsqr_sqrt.
 
319
  rewrite Rsqr_inv.
 
320
  unfold Rsqr in |- *; repeat rewrite Rinv_mult_distr;
 
321
    repeat rewrite Rmult_assoc.
 
322
  rewrite (Rmult_comm a); repeat rewrite Rmult_assoc.
 
323
  rewrite <- Rinv_l_sym.
 
324
  rewrite Rmult_1_r; unfold Rminus in |- *; rewrite Rmult_plus_distr_r.
 
325
  rewrite Ropp_mult_distr_l_reverse; repeat rewrite Rmult_assoc;
 
326
    pattern 2 at 2 in |- *; rewrite (Rmult_comm 2).
 
327
  repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
 
328
  rewrite Rmult_1_r;
 
329
    rewrite
 
330
      (Rmult_plus_distr_r (- b) (- sqrt (b * b + - (2 * (2 * (a * c)))))
 
331
        (/ 2 * / a)).
 
332
  rewrite Rmult_plus_distr_l; repeat rewrite Rplus_assoc.
 
333
  rewrite Ropp_mult_distr_l_reverse; rewrite Ropp_involutive.
 
334
  replace
 
335
  (b * (sqrt (b * b + - (2 * (2 * (a * c)))) * (/ 2 * / a)) +
 
336
    (b * (- b * (/ 2 * / a)) +
 
337
      (b * (- sqrt (b * b + - (2 * (2 * (a * c)))) * (/ 2 * / a)) + c))) with
 
338
  (b * (- b * (/ 2 * / a)) + c).
 
339
  repeat rewrite <- Rplus_assoc; replace (b * b + b * b) with (2 * (b * b)).
 
340
  rewrite Rmult_plus_distr_r; repeat rewrite Rmult_assoc;
 
341
    rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc; 
 
342
      rewrite <- Rinv_l_sym.
 
343
  rewrite Ropp_mult_distr_l_reverse; repeat rewrite Rmult_assoc.
 
344
  rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
 
345
  rewrite Rmult_1_r; rewrite (Rmult_comm (/ 2)); repeat rewrite Rmult_assoc.
 
346
  rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
 
347
  rewrite Rmult_1_r; repeat rewrite Rmult_assoc; rewrite (Rmult_comm a);
 
348
    rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
 
349
  rewrite Rmult_1_r; rewrite <- Rmult_opp_opp; ring.
 
350
  apply (cond_nonzero a).
 
351
  discrR.
 
352
  discrR.
 
353
  discrR.
 
354
  ring.
 
355
  ring.
 
356
  discrR.
 
357
  apply (cond_nonzero a).
 
358
  discrR.
 
359
  discrR.
 
360
  apply (cond_nonzero a).
 
361
  apply prod_neq_R0; discrR || apply (cond_nonzero a).
 
362
  apply prod_neq_R0; discrR || apply (cond_nonzero a).
 
363
  apply prod_neq_R0; discrR || apply (cond_nonzero a).
 
364
  assumption.
 
365
Qed.
 
366
 
 
367
Lemma Rsqr_sol_eq_0_0 :
 
368
  forall (a:nonzeroreal) (b c x:R),
 
369
    Delta_is_pos a b c ->
 
370
    a * Rsqr x + b * x + c = 0 -> x = sol_x1 a b c \/ x = sol_x2 a b c.
 
371
Proof.
 
372
  intros; rewrite (canonical_Rsqr a b c x) in H0; rewrite Rplus_comm in H0;
 
373
    generalize
 
374
      (Rplus_opp_r_uniq ((4 * a * c - Rsqr b) / (4 * a))
 
375
        (a * Rsqr (x + b / (2 * a))) H0); cut (Rsqr b - 4 * a * c = Delta a b c).
 
376
  intro;
 
377
    replace (- ((4 * a * c - Rsqr b) / (4 * a))) with
 
378
    ((Rsqr b - 4 * a * c) / (4 * a)).
 
379
  rewrite H1; intro;
 
380
    generalize
 
381
      (Rmult_eq_compat_l (/ a) (a * Rsqr (x + b / (2 * a)))
 
382
        (Delta a b c / (4 * a)) H2);
 
383
      replace (/ a * (a * Rsqr (x + b / (2 * a)))) with (Rsqr (x + b / (2 * a))).
 
384
  replace (/ a * (Delta a b c / (4 * a))) with
 
385
  (Rsqr (sqrt (Delta a b c) / (2 * a))).
 
386
  intro;
 
387
    generalize (Rsqr_eq (x + b / (2 * a)) (sqrt (Delta a b c) / (2 * a)) H3);
 
388
      intro; elim H4; intro.
 
389
  left; unfold sol_x1 in |- *;
 
390
    generalize
 
391
      (Rplus_eq_compat_l (- (b / (2 * a))) (x + b / (2 * a))
 
392
        (sqrt (Delta a b c) / (2 * a)) H5);
 
393
      replace (- (b / (2 * a)) + (x + b / (2 * a))) with x.
 
394
  intro; rewrite H6; unfold Rdiv in |- *; ring.
 
395
  ring.
 
396
  right; unfold sol_x2 in |- *;
 
397
    generalize
 
398
      (Rplus_eq_compat_l (- (b / (2 * a))) (x + b / (2 * a))
 
399
        (- (sqrt (Delta a b c) / (2 * a))) H5);
 
400
      replace (- (b / (2 * a)) + (x + b / (2 * a))) with x.
 
401
  intro; rewrite H6; unfold Rdiv in |- *; ring.
 
402
  ring.
 
403
  rewrite Rsqr_div.
 
404
  rewrite Rsqr_sqrt.
 
405
  unfold Rdiv in |- *.
 
406
  repeat rewrite Rmult_assoc.
 
407
  rewrite (Rmult_comm (/ a)).
 
408
  rewrite Rmult_assoc.
 
409
  rewrite <- Rinv_mult_distr.
 
410
  replace (2 * (2 * a) * a) with (Rsqr (2 * a)).
 
411
  reflexivity.
 
412
  ring_Rsqr.
 
413
  rewrite <- Rmult_assoc; apply prod_neq_R0;
 
414
    [ discrR | apply (cond_nonzero a) ].
 
415
  apply (cond_nonzero a).
 
416
  assumption.
 
417
  apply prod_neq_R0; [ discrR | apply (cond_nonzero a) ].
 
418
  rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym.
 
419
  symmetry  in |- *; apply Rmult_1_l.
 
420
  apply (cond_nonzero a).
 
421
  unfold Rdiv in |- *; rewrite <- Ropp_mult_distr_l_reverse.
 
422
  rewrite Ropp_minus_distr.
 
423
  reflexivity.
 
424
  reflexivity.
 
425
Qed.