Imported Upstream version 8.1~gammaupstream/8.1.gamma

1 files changed, 316 insertions, 291 deletions

diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v
index cb372840..736365a0 100644
--- a/theories/Reals/R_sqrt.v
+++ b/theories/Reals/R_sqrt.v
@@ -6,219 +6,242 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: R_sqrt.v 6295 2004-11-12 16:40:39Z gregoire $ i*)
+(*i $Id: R_sqrt.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rsqrt_def. Open Local Scope R_scope.
 
-(* Here is a continuous extension of Rsqrt on R *)
+(** * Continuous extension of Rsqrt on R *)
 Definition sqrt (x:R) : R :=
   match Rcase_abs x with
-  | left _ => 0
-  | right a => Rsqrt (mknonnegreal x (Rge_le _ _ a))
+    | left _ => 0
+    | right a => Rsqrt (mknonnegreal x (Rge_le _ _ a))
   end.
 
 Lemma sqrt_positivity : forall x:R, 0 <= x -> 0 <= sqrt x.
-intros.
-unfold sqrt in |- *.
-case (Rcase_abs x); intro.
-elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ r H)).
-apply Rsqrt_positivity.
+Proof.
+  intros.
+  unfold sqrt in |- *.
+  case (Rcase_abs x); intro.
+  elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ r H)).
+  apply Rsqrt_positivity.
 Qed.
 
 Lemma sqrt_sqrt : forall x:R, 0 <= x -> sqrt x * sqrt x = x.
-intros.
-unfold sqrt in |- *.
-case (Rcase_abs x); intro.
-elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ r H)).
-rewrite Rsqrt_Rsqrt; reflexivity.
+Proof.
+  intros.
+  unfold sqrt in |- *.
+  case (Rcase_abs x); intro.
+  elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ r H)).
+  rewrite Rsqrt_Rsqrt; reflexivity.
 Qed.
 
 Lemma sqrt_0 : sqrt 0 = 0.
-apply Rsqr_eq_0; unfold Rsqr in |- *; apply sqrt_sqrt; right; reflexivity. 
+Proof.
+  apply Rsqr_eq_0; unfold Rsqr in |- *; apply sqrt_sqrt; right; reflexivity. 
 Qed.
 
 Lemma sqrt_1 : sqrt 1 = 1.
-apply (Rsqr_inj (sqrt 1) 1);
- [ apply sqrt_positivity; left
- | left
- | unfold Rsqr in |- *; rewrite sqrt_sqrt; [ ring | left ] ]; 
- apply Rlt_0_1.
+Proof.
+  apply (Rsqr_inj (sqrt 1) 1);
+    [ apply sqrt_positivity; left
+      | left
+      | unfold Rsqr in |- *; rewrite sqrt_sqrt; [ ring | left ] ]; 
+    apply Rlt_0_1.
 Qed.
 
 Lemma sqrt_eq_0 : forall x:R, 0 <= x -> sqrt x = 0 -> x = 0.
-intros; cut (Rsqr (sqrt x) = 0).
-intro; unfold Rsqr in H1; rewrite sqrt_sqrt in H1; assumption.
-rewrite H0; apply Rsqr_0.
+Proof.
+  intros; cut (Rsqr (sqrt x) = 0).
+  intro; unfold Rsqr in H1; rewrite sqrt_sqrt in H1; assumption.
+  rewrite H0; apply Rsqr_0.
 Qed.
 
 Lemma sqrt_lem_0 : forall x y:R, 0 <= x -> 0 <= y -> sqrt x = y -> y * y = x.
-intros; rewrite <- H1; apply (sqrt_sqrt x H).
+Proof.
+  intros; rewrite <- H1; apply (sqrt_sqrt x H).
 Qed.
 
-Lemma sqtr_lem_1 : forall x y:R, 0 <= x -> 0 <= y -> y * y = x -> sqrt x = y.
-intros; apply Rsqr_inj;
- [ apply (sqrt_positivity x H)
- | assumption
- | unfold Rsqr in |- *; rewrite H1; apply (sqrt_sqrt x H) ].
+Lemma sqrt_lem_1 : forall x y:R, 0 <= x -> 0 <= y -> y * y = x -> sqrt x = y.
+Proof.
+  intros; apply Rsqr_inj;
+    [ apply (sqrt_positivity x H)
+      | assumption
+      | unfold Rsqr in |- *; rewrite H1; apply (sqrt_sqrt x H) ].
 Qed.
 
 Lemma sqrt_def : forall x:R, 0 <= x -> sqrt x * sqrt x = x.
-intros; apply (sqrt_sqrt x H).
+Proof.
+  intros; apply (sqrt_sqrt x H).
 Qed.
 
 Lemma sqrt_square : forall x:R, 0 <= x -> sqrt (x * x) = x.
-intros;
- apply
-  (Rsqr_inj (sqrt (Rsqr x)) x (sqrt_positivity (Rsqr x) (Rle_0_sqr x)) H);
- unfold Rsqr in |- *; apply (sqrt_sqrt (Rsqr x) (Rle_0_sqr x)).
+Proof.
+  intros;
+    apply
+      (Rsqr_inj (sqrt (Rsqr x)) x (sqrt_positivity (Rsqr x) (Rle_0_sqr x)) H);
+      unfold Rsqr in |- *; apply (sqrt_sqrt (Rsqr x) (Rle_0_sqr x)).
 Qed.
 
 Lemma sqrt_Rsqr : forall x:R, 0 <= x -> sqrt (Rsqr x) = x.
-intros; unfold Rsqr in |- *; apply sqrt_square; assumption.
+Proof.
+  intros; unfold Rsqr in |- *; apply sqrt_square; assumption.
 Qed.
 
 Lemma sqrt_Rsqr_abs : forall x:R, sqrt (Rsqr x) = Rabs x.
-intro x; rewrite Rsqr_abs; apply sqrt_Rsqr; apply Rabs_pos.
+Proof.
+  intro x; rewrite Rsqr_abs; apply sqrt_Rsqr; apply Rabs_pos.
 Qed.
 
 Lemma Rsqr_sqrt : forall x:R, 0 <= x -> Rsqr (sqrt x) = x.
-intros x H1; unfold Rsqr in |- *; apply (sqrt_sqrt x H1).
+Proof.
+  intros x H1; unfold Rsqr in |- *; apply (sqrt_sqrt x H1).
 Qed.
 
 Lemma sqrt_mult :
- forall x y:R, 0 <= x -> 0 <= y -> sqrt (x * y) = sqrt x * sqrt y.
-intros x y H1 H2;
- apply
-  (Rsqr_inj (sqrt (x * y)) (sqrt x * sqrt y)
-     (sqrt_positivity (x * y) (Rmult_le_pos x y H1 H2))
-     (Rmult_le_pos (sqrt x) (sqrt y) (sqrt_positivity x H1)
-        (sqrt_positivity y H2))); rewrite Rsqr_mult; 
- repeat rewrite Rsqr_sqrt;
- [ ring | assumption | assumption | apply (Rmult_le_pos x y H1 H2) ].
+  forall x y:R, 0 <= x -> 0 <= y -> sqrt (x * y) = sqrt x * sqrt y.
+Proof.
+  intros x y H1 H2;
+    apply
+      (Rsqr_inj (sqrt (x * y)) (sqrt x * sqrt y)
+        (sqrt_positivity (x * y) (Rmult_le_pos x y H1 H2))
+        (Rmult_le_pos (sqrt x) (sqrt y) (sqrt_positivity x H1)
+          (sqrt_positivity y H2))); rewrite Rsqr_mult; 
+      repeat rewrite Rsqr_sqrt;
+        [ ring | assumption | assumption | apply (Rmult_le_pos x y H1 H2) ].
 Qed.
 
 Lemma sqrt_lt_R0 : forall x:R, 0 < x -> 0 < sqrt x.
-intros x H1; apply Rsqr_incrst_0;
- [ rewrite Rsqr_0; rewrite Rsqr_sqrt; [ assumption | left; assumption ]
- | right; reflexivity
- | apply (sqrt_positivity x (Rlt_le 0 x H1)) ].
+Proof.
+  intros x H1; apply Rsqr_incrst_0;
+    [ rewrite Rsqr_0; rewrite Rsqr_sqrt; [ assumption | left; assumption ]
+      | right; reflexivity
+      | apply (sqrt_positivity x (Rlt_le 0 x H1)) ].
 Qed.
 
 Lemma sqrt_div :
- forall x y:R, 0 <= x -> 0 < y -> sqrt (x / y) = sqrt x / sqrt y.
-intros x y H1 H2; apply Rsqr_inj;
- [ apply sqrt_positivity; apply (Rmult_le_pos x (/ y));
-    [ assumption
-    | generalize (Rinv_0_lt_compat y H2); clear H2; intro H2; left;
-       assumption ]
- | apply (Rmult_le_pos (sqrt x) (/ sqrt y));
-    [ apply (sqrt_positivity x H1)
-    | generalize (sqrt_lt_R0 y H2); clear H2; intro H2;
-       generalize (Rinv_0_lt_compat (sqrt y) H2); clear H2; 
-       intro H2; left; assumption ]
- | rewrite Rsqr_div; repeat rewrite Rsqr_sqrt;
-    [ reflexivity
-    | left; assumption
-    | assumption
-    | generalize (Rinv_0_lt_compat y H2); intro H3;
-       generalize (Rlt_le 0 (/ y) H3); intro H4;
-       apply (Rmult_le_pos x (/ y) H1 H4)
-    | red in |- *; intro H3; generalize (Rlt_le 0 y H2); intro H4;
-       generalize (sqrt_eq_0 y H4 H3); intro H5; rewrite H5 in H2;
-       elim (Rlt_irrefl 0 H2) ] ].
+  forall x y:R, 0 <= x -> 0 < y -> sqrt (x / y) = sqrt x / sqrt y.
+Proof.
+  intros x y H1 H2; apply Rsqr_inj;
+    [ apply sqrt_positivity; apply (Rmult_le_pos x (/ y));
+      [ assumption
+        | generalize (Rinv_0_lt_compat y H2); clear H2; intro H2; left;
+          assumption ]
+      | apply (Rmult_le_pos (sqrt x) (/ sqrt y));
+        [ apply (sqrt_positivity x H1)
+          | generalize (sqrt_lt_R0 y H2); clear H2; intro H2;
+            generalize (Rinv_0_lt_compat (sqrt y) H2); clear H2; 
+              intro H2; left; assumption ]
+      | rewrite Rsqr_div; repeat rewrite Rsqr_sqrt;
+        [ reflexivity
+          | left; assumption
+          | assumption
+          | generalize (Rinv_0_lt_compat y H2); intro H3;
+            generalize (Rlt_le 0 (/ y) H3); intro H4;
+              apply (Rmult_le_pos x (/ y) H1 H4)
+          | red in |- *; intro H3; generalize (Rlt_le 0 y H2); intro H4;
+            generalize (sqrt_eq_0 y H4 H3); intro H5; rewrite H5 in H2;
+              elim (Rlt_irrefl 0 H2) ] ].
 Qed.
 
 Lemma sqrt_lt_0 : forall x y:R, 0 <= x -> 0 <= y -> sqrt x < sqrt y -> x < y.
-intros x y H1 H2 H3;
- generalize
-  (Rsqr_incrst_1 (sqrt x) (sqrt y) H3 (sqrt_positivity x H1)
-     (sqrt_positivity y H2)); intro H4; rewrite (Rsqr_sqrt x H1) in H4;
- rewrite (Rsqr_sqrt y H2) in H4; assumption.
+Proof.
+  intros x y H1 H2 H3;
+    generalize
+      (Rsqr_incrst_1 (sqrt x) (sqrt y) H3 (sqrt_positivity x H1)
+        (sqrt_positivity y H2)); intro H4; rewrite (Rsqr_sqrt x H1) in H4;
+      rewrite (Rsqr_sqrt y H2) in H4; assumption.
 Qed.
 
 Lemma sqrt_lt_1 : forall x y:R, 0 <= x -> 0 <= y -> x < y -> sqrt x < sqrt y.
-intros x y H1 H2 H3; apply Rsqr_incrst_0;
- [ rewrite (Rsqr_sqrt x H1); rewrite (Rsqr_sqrt y H2); assumption
- | apply (sqrt_positivity x H1)
- | apply (sqrt_positivity y H2) ].
+Proof.
+  intros x y H1 H2 H3; apply Rsqr_incrst_0;
+    [ rewrite (Rsqr_sqrt x H1); rewrite (Rsqr_sqrt y H2); assumption
+      | apply (sqrt_positivity x H1)
+      | apply (sqrt_positivity y H2) ].
 Qed.
 
 Lemma sqrt_le_0 :
- forall x y:R, 0 <= x -> 0 <= y -> sqrt x <= sqrt y -> x <= y.
-intros x y H1 H2 H3;
- generalize
-  (Rsqr_incr_1 (sqrt x) (sqrt y) H3 (sqrt_positivity x H1)
-     (sqrt_positivity y H2)); intro H4; rewrite (Rsqr_sqrt x H1) in H4;
- rewrite (Rsqr_sqrt y H2) in H4; assumption.
+  forall x y:R, 0 <= x -> 0 <= y -> sqrt x <= sqrt y -> x <= y.
+Proof.
+  intros x y H1 H2 H3;
+    generalize
+      (Rsqr_incr_1 (sqrt x) (sqrt y) H3 (sqrt_positivity x H1)
+        (sqrt_positivity y H2)); intro H4; rewrite (Rsqr_sqrt x H1) in H4;
+      rewrite (Rsqr_sqrt y H2) in H4; assumption.
 Qed.
 
 Lemma sqrt_le_1 :
- forall x y:R, 0 <= x -> 0 <= y -> x <= y -> sqrt x <= sqrt y.
-intros x y H1 H2 H3; apply Rsqr_incr_0;
- [ rewrite (Rsqr_sqrt x H1); rewrite (Rsqr_sqrt y H2); assumption
- | apply (sqrt_positivity x H1)
- | apply (sqrt_positivity y H2) ].
+  forall x y:R, 0 <= x -> 0 <= y -> x <= y -> sqrt x <= sqrt y.
+Proof.
+  intros x y H1 H2 H3; apply Rsqr_incr_0;
+    [ rewrite (Rsqr_sqrt x H1); rewrite (Rsqr_sqrt y H2); assumption
+      | apply (sqrt_positivity x H1)
+      | apply (sqrt_positivity y H2) ].
 Qed.
 
 Lemma sqrt_inj : forall x y:R, 0 <= x -> 0 <= y -> sqrt x = sqrt y -> x = y.
-intros; cut (Rsqr (sqrt x) = Rsqr (sqrt y)).
-intro; rewrite (Rsqr_sqrt x H) in H2; rewrite (Rsqr_sqrt y H0) in H2;
- assumption.
-rewrite H1; reflexivity.
+Proof.
+  intros; cut (Rsqr (sqrt x) = Rsqr (sqrt y)).
+  intro; rewrite (Rsqr_sqrt x H) in H2; rewrite (Rsqr_sqrt y H0) in H2;
+    assumption.
+  rewrite H1; reflexivity.
 Qed.
 
 Lemma sqrt_less : forall x:R, 0 <= x -> 1 < x -> sqrt x < x.
-intros x H1 H2; generalize (sqrt_lt_1 1 x (Rlt_le 0 1 Rlt_0_1) H1 H2);
- intro H3; rewrite sqrt_1 in H3; generalize (Rmult_ne (sqrt x)); 
- intro H4; elim H4; intros H5 H6; rewrite <- H5; pattern x at 2 in |- *;
- rewrite <- (sqrt_def x H1);
- apply
-  (Rmult_lt_compat_l (sqrt x) 1 (sqrt x)
-     (sqrt_lt_R0 x (Rlt_trans 0 1 x Rlt_0_1 H2)) H3).
+Proof.
+  intros x H1 H2; generalize (sqrt_lt_1 1 x (Rlt_le 0 1 Rlt_0_1) H1 H2);
+    intro H3; rewrite sqrt_1 in H3; generalize (Rmult_ne (sqrt x)); 
+      intro H4; elim H4; intros H5 H6; rewrite <- H5; pattern x at 2 in |- *;
+        rewrite <- (sqrt_def x H1);
+          apply
+            (Rmult_lt_compat_l (sqrt x) 1 (sqrt x)
+              (sqrt_lt_R0 x (Rlt_trans 0 1 x Rlt_0_1 H2)) H3).
 Qed.
 
 Lemma sqrt_more : forall x:R, 0 < x -> x < 1 -> x < sqrt x.
-intros x H1 H2;
- generalize (sqrt_lt_1 x 1 (Rlt_le 0 x H1) (Rlt_le 0 1 Rlt_0_1) H2); 
- intro H3; rewrite sqrt_1 in H3; generalize (Rmult_ne (sqrt x)); 
- intro H4; elim H4; intros H5 H6; rewrite <- H5; pattern x at 1 in |- *;
- rewrite <- (sqrt_def x (Rlt_le 0 x H1));
- apply (Rmult_lt_compat_l (sqrt x) (sqrt x) 1 (sqrt_lt_R0 x H1) H3).
+Proof.
+  intros x H1 H2;
+    generalize (sqrt_lt_1 x 1 (Rlt_le 0 x H1) (Rlt_le 0 1 Rlt_0_1) H2); 
+      intro H3; rewrite sqrt_1 in H3; generalize (Rmult_ne (sqrt x)); 
+        intro H4; elim H4; intros H5 H6; rewrite <- H5; pattern x at 1 in |- *;
+          rewrite <- (sqrt_def x (Rlt_le 0 x H1));
+            apply (Rmult_lt_compat_l (sqrt x) (sqrt x) 1 (sqrt_lt_R0 x H1) H3).
 Qed.
 
 Lemma sqrt_cauchy :
- forall a b c d:R,
-   a * c + b * d <= sqrt (Rsqr a + Rsqr b) * sqrt (Rsqr c + Rsqr d).
-intros a b c d; apply Rsqr_incr_0_var;
- [ rewrite Rsqr_mult; repeat rewrite Rsqr_sqrt; unfold Rsqr in |- *;
-    [ replace ((a * c + b * d) * (a * c + b * d)) with
-       (a * a * c * c + b * b * d * d + 2 * a * b * c * d);
-       [ replace ((a * a + b * b) * (c * c + d * d)) with
+  forall a b c d:R,
+    a * c + b * d <= sqrt (Rsqr a + Rsqr b) * sqrt (Rsqr c + Rsqr d).
+Proof.
+  intros a b c d; apply Rsqr_incr_0_var;
+    [ rewrite Rsqr_mult; repeat rewrite Rsqr_sqrt; unfold Rsqr in |- *;
+      [ replace ((a * c + b * d) * (a * c + b * d)) with
+        (a * a * c * c + b * b * d * d + 2 * a * b * c * d);
+        [ replace ((a * a + b * b) * (c * c + d * d)) with
           (a * a * c * c + b * b * d * d + (a * a * d * d + b * b * c * c));
           [ apply Rplus_le_compat_l;
-             replace (a * a * d * d + b * b * c * c) with
-              (2 * a * b * c * d +
-               (a * a * d * d + b * b * c * c - 2 * a * b * c * d));
-             [ pattern (2 * a * b * c * d) at 1 in |- *; rewrite <- Rplus_0_r;
-                apply Rplus_le_compat_l;
+            replace (a * a * d * d + b * b * c * c) with
+            (2 * a * b * c * d +
+              (a * a * d * d + b * b * c * c - 2 * a * b * c * d));
+            [ pattern (2 * a * b * c * d) at 1 in |- *; rewrite <- Rplus_0_r;
+              apply Rplus_le_compat_l;
                 replace (a * a * d * d + b * b * c * c - 2 * a * b * c * d)
-                 with (Rsqr (a * d - b * c));
+              with (Rsqr (a * d - b * c));
                 [ apply Rle_0_sqr | unfold Rsqr in |- *; ring ]
-             | ring ]
+              | ring ]
+            | ring ]
           | ring ]
-       | ring ]
-    | apply
-       (Rplus_le_le_0_compat (Rsqr c) (Rsqr d) (Rle_0_sqr c) (Rle_0_sqr d))
-    | apply
-       (Rplus_le_le_0_compat (Rsqr a) (Rsqr b) (Rle_0_sqr a) (Rle_0_sqr b)) ]
- | apply Rmult_le_pos; apply sqrt_positivity; apply Rplus_le_le_0_compat;
-    apply Rle_0_sqr ].
+        | apply
+          (Rplus_le_le_0_compat (Rsqr c) (Rsqr d) (Rle_0_sqr c) (Rle_0_sqr d))
+        | apply
+          (Rplus_le_le_0_compat (Rsqr a) (Rsqr b) (Rle_0_sqr a) (Rle_0_sqr b)) ]
+      | apply Rmult_le_pos; apply sqrt_positivity; apply Rplus_le_le_0_compat;
+        apply Rle_0_sqr ].
 Qed.
 
 (************************************************************)
-(* Resolution of [a*X^2+b*X+c=0]                            *)
+(** * Resolution of [a*X^2+b*X+c=0]                         *)
 (************************************************************)
 
 Definition Delta (a:nonzeroreal) (b c:R) : R := Rsqr b - 4 * a * c.
@@ -232,168 +255,170 @@ Definition sol_x2 (a:nonzeroreal) (b c:R) : R :=
   (- b - sqrt (Delta a b c)) / (2 * a).
 
 Lemma Rsqr_sol_eq_0_1 :
- forall (a:nonzeroreal) (b c x:R),
-   Delta_is_pos a b c ->
-   x = sol_x1 a b c \/ x = sol_x2 a b c -> a * Rsqr x + b * x + c = 0.
-intros; elim H0; intro.
-unfold sol_x1 in H1; unfold Delta in H1; rewrite H1; unfold Rdiv in |- *;
- repeat rewrite Rsqr_mult; rewrite Rsqr_plus; rewrite <- Rsqr_neg;
- rewrite Rsqr_sqrt.
-rewrite Rsqr_inv.
-unfold Rsqr in |- *; repeat rewrite Rinv_mult_distr.
-repeat rewrite Rmult_assoc; rewrite (Rmult_comm a).
-repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
-rewrite Rmult_1_r; rewrite Rmult_plus_distr_r.
-repeat rewrite Rmult_assoc.
-pattern 2 at 2 in |- *; rewrite (Rmult_comm 2).
-repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
-rewrite Rmult_1_r.
-rewrite
- (Rmult_plus_distr_r (- b) (sqrt (b * b - 2 * (2 * (a * c)))) (/ 2 * / a))
- .
-rewrite Rmult_plus_distr_l; repeat rewrite Rplus_assoc.
-replace
- (- b * (sqrt (b * b - 2 * (2 * (a * c))) * (/ 2 * / a)) +
-  (b * (- b * (/ 2 * / a)) +
-   (b * (sqrt (b * b - 2 * (2 * (a * c))) * (/ 2 * / a)) + c))) with
- (b * (- b * (/ 2 * / a)) + c).
-unfold Rminus in |- *; repeat rewrite <- Rplus_assoc.
-replace (b * b + b * b) with (2 * (b * b)).
-rewrite Rmult_plus_distr_r; repeat rewrite Rmult_assoc.
-rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc.
-rewrite <- Rinv_l_sym.
-rewrite Rmult_1_r.
-rewrite Ropp_mult_distr_l_reverse; repeat rewrite Rmult_assoc;
- rewrite (Rmult_comm 2).
-repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
-rewrite Rmult_1_r; rewrite (Rmult_comm (/ 2)); repeat rewrite Rmult_assoc;
- rewrite (Rmult_comm 2).
-repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
-rewrite Rmult_1_r; repeat rewrite Rmult_assoc.
-rewrite (Rmult_comm a); rewrite Rmult_assoc.
-rewrite <- Rinv_l_sym.
-rewrite Rmult_1_r; rewrite <- Rmult_opp_opp.
-ring.
-apply (cond_nonzero a).
-discrR.
-discrR.
-discrR.
-ring.
-ring.
-discrR.
-apply (cond_nonzero a).
-discrR.
-apply (cond_nonzero a).
-apply prod_neq_R0; [ discrR | apply (cond_nonzero a) ].
-apply prod_neq_R0; [ discrR | apply (cond_nonzero a) ].
-apply prod_neq_R0; [ discrR | apply (cond_nonzero a) ].
-assumption.
-unfold sol_x2 in H1; unfold Delta in H1; rewrite H1; unfold Rdiv in |- *;
- repeat rewrite Rsqr_mult; rewrite Rsqr_minus; rewrite <- Rsqr_neg;
- rewrite Rsqr_sqrt.
-rewrite Rsqr_inv.
-unfold Rsqr in |- *; repeat rewrite Rinv_mult_distr;
- repeat rewrite Rmult_assoc.
-rewrite (Rmult_comm a); repeat rewrite Rmult_assoc.
-rewrite <- Rinv_l_sym.
-rewrite Rmult_1_r; unfold Rminus in |- *; rewrite Rmult_plus_distr_r.
-rewrite Ropp_mult_distr_l_reverse; repeat rewrite Rmult_assoc;
- pattern 2 at 2 in |- *; rewrite (Rmult_comm 2).
-repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
-rewrite Rmult_1_r;
- rewrite
-  (Rmult_plus_distr_r (- b) (- sqrt (b * b + - (2 * (2 * (a * c)))))
-     (/ 2 * / a)).
-rewrite Rmult_plus_distr_l; repeat rewrite Rplus_assoc.
-rewrite Ropp_mult_distr_l_reverse; rewrite Ropp_involutive.
-replace
- (b * (sqrt (b * b + - (2 * (2 * (a * c)))) * (/ 2 * / a)) +
-  (b * (- b * (/ 2 * / a)) +
-   (b * (- sqrt (b * b + - (2 * (2 * (a * c)))) * (/ 2 * / a)) + c))) with
- (b * (- b * (/ 2 * / a)) + c).
-repeat rewrite <- Rplus_assoc; replace (b * b + b * b) with (2 * (b * b)).
-rewrite Rmult_plus_distr_r; repeat rewrite Rmult_assoc;
- rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc; 
- rewrite <- Rinv_l_sym.
-rewrite Ropp_mult_distr_l_reverse; repeat rewrite Rmult_assoc.
-rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
-rewrite Rmult_1_r; rewrite (Rmult_comm (/ 2)); repeat rewrite Rmult_assoc.
-rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
-rewrite Rmult_1_r; repeat rewrite Rmult_assoc; rewrite (Rmult_comm a);
- rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
-rewrite Rmult_1_r; rewrite <- Rmult_opp_opp; ring.
-apply (cond_nonzero a).
-discrR.
-discrR.
-discrR.
-ring.
-ring.
-discrR.
-apply (cond_nonzero a).
-discrR.
-discrR.
-apply (cond_nonzero a).
-apply prod_neq_R0; discrR || apply (cond_nonzero a).
-apply prod_neq_R0; discrR || apply (cond_nonzero a).
-apply prod_neq_R0; discrR || apply (cond_nonzero a).
-assumption.
+  forall (a:nonzeroreal) (b c x:R),
+    Delta_is_pos a b c ->
+    x = sol_x1 a b c \/ x = sol_x2 a b c -> a * Rsqr x + b * x + c = 0.
+Proof.
+  intros; elim H0; intro.
+  unfold sol_x1 in H1; unfold Delta in H1; rewrite H1; unfold Rdiv in |- *;
+    repeat rewrite Rsqr_mult; rewrite Rsqr_plus; rewrite <- Rsqr_neg;
+      rewrite Rsqr_sqrt.
+  rewrite Rsqr_inv.
+  unfold Rsqr in |- *; repeat rewrite Rinv_mult_distr.
+  repeat rewrite Rmult_assoc; rewrite (Rmult_comm a).
+  repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
+  rewrite Rmult_1_r; rewrite Rmult_plus_distr_r.
+  repeat rewrite Rmult_assoc.
+  pattern 2 at 2 in |- *; rewrite (Rmult_comm 2).
+  repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
+  rewrite Rmult_1_r.
+  rewrite
+    (Rmult_plus_distr_r (- b) (sqrt (b * b - 2 * (2 * (a * c)))) (/ 2 * / a))
+    .
+  rewrite Rmult_plus_distr_l; repeat rewrite Rplus_assoc.
+  replace
+  (- b * (sqrt (b * b - 2 * (2 * (a * c))) * (/ 2 * / a)) +
+    (b * (- b * (/ 2 * / a)) +
+      (b * (sqrt (b * b - 2 * (2 * (a * c))) * (/ 2 * / a)) + c))) with
+  (b * (- b * (/ 2 * / a)) + c).
+  unfold Rminus in |- *; repeat rewrite <- Rplus_assoc.
+  replace (b * b + b * b) with (2 * (b * b)).
+  rewrite Rmult_plus_distr_r; repeat rewrite Rmult_assoc.
+  rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc.
+  rewrite <- Rinv_l_sym.
+  rewrite Rmult_1_r.
+  rewrite Ropp_mult_distr_l_reverse; repeat rewrite Rmult_assoc;
+    rewrite (Rmult_comm 2).
+  repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
+  rewrite Rmult_1_r; rewrite (Rmult_comm (/ 2)); repeat rewrite Rmult_assoc;
+    rewrite (Rmult_comm 2).
+  repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
+  rewrite Rmult_1_r; repeat rewrite Rmult_assoc.
+  rewrite (Rmult_comm a); rewrite Rmult_assoc.
+  rewrite <- Rinv_l_sym.
+  rewrite Rmult_1_r; rewrite <- Rmult_opp_opp.
+  ring.
+  apply (cond_nonzero a).
+  discrR.
+  discrR.
+  discrR.
+  ring.
+  ring.
+  discrR.
+  apply (cond_nonzero a).
+  discrR.
+  apply (cond_nonzero a).
+  apply prod_neq_R0; [ discrR | apply (cond_nonzero a) ].
+  apply prod_neq_R0; [ discrR | apply (cond_nonzero a) ].
+  apply prod_neq_R0; [ discrR | apply (cond_nonzero a) ].
+  assumption.
+  unfold sol_x2 in H1; unfold Delta in H1; rewrite H1; unfold Rdiv in |- *;
+    repeat rewrite Rsqr_mult; rewrite Rsqr_minus; rewrite <- Rsqr_neg;
+      rewrite Rsqr_sqrt.
+  rewrite Rsqr_inv.
+  unfold Rsqr in |- *; repeat rewrite Rinv_mult_distr;
+    repeat rewrite Rmult_assoc.
+  rewrite (Rmult_comm a); repeat rewrite Rmult_assoc.
+  rewrite <- Rinv_l_sym.
+  rewrite Rmult_1_r; unfold Rminus in |- *; rewrite Rmult_plus_distr_r.
+  rewrite Ropp_mult_distr_l_reverse; repeat rewrite Rmult_assoc;
+    pattern 2 at 2 in |- *; rewrite (Rmult_comm 2).
+  repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
+  rewrite Rmult_1_r;
+    rewrite
+      (Rmult_plus_distr_r (- b) (- sqrt (b * b + - (2 * (2 * (a * c)))))
+        (/ 2 * / a)).
+  rewrite Rmult_plus_distr_l; repeat rewrite Rplus_assoc.
+  rewrite Ropp_mult_distr_l_reverse; rewrite Ropp_involutive.
+  replace
+  (b * (sqrt (b * b + - (2 * (2 * (a * c)))) * (/ 2 * / a)) +
+    (b * (- b * (/ 2 * / a)) +
+      (b * (- sqrt (b * b + - (2 * (2 * (a * c)))) * (/ 2 * / a)) + c))) with
+  (b * (- b * (/ 2 * / a)) + c).
+  repeat rewrite <- Rplus_assoc; replace (b * b + b * b) with (2 * (b * b)).
+  rewrite Rmult_plus_distr_r; repeat rewrite Rmult_assoc;
+    rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc; 
+      rewrite <- Rinv_l_sym.
+  rewrite Ropp_mult_distr_l_reverse; repeat rewrite Rmult_assoc.
+  rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
+  rewrite Rmult_1_r; rewrite (Rmult_comm (/ 2)); repeat rewrite Rmult_assoc.
+  rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
+  rewrite Rmult_1_r; repeat rewrite Rmult_assoc; rewrite (Rmult_comm a);
+    rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
+  rewrite Rmult_1_r; rewrite <- Rmult_opp_opp; ring.
+  apply (cond_nonzero a).
+  discrR.
+  discrR.
+  discrR.
+  ring.
+  ring.
+  discrR.
+  apply (cond_nonzero a).
+  discrR.
+  discrR.
+  apply (cond_nonzero a).
+  apply prod_neq_R0; discrR || apply (cond_nonzero a).
+  apply prod_neq_R0; discrR || apply (cond_nonzero a).
+  apply prod_neq_R0; discrR || apply (cond_nonzero a).
+  assumption.
 Qed.
 
 Lemma Rsqr_sol_eq_0_0 :
- forall (a:nonzeroreal) (b c x:R),
-   Delta_is_pos a b c ->
-   a * Rsqr x + b * x + c = 0 -> x = sol_x1 a b c \/ x = sol_x2 a b c.
-intros; rewrite (canonical_Rsqr a b c x) in H0; rewrite Rplus_comm in H0;
- generalize
-  (Rplus_opp_r_uniq ((4 * a * c - Rsqr b) / (4 * a))
-     (a * Rsqr (x + b / (2 * a))) H0); cut (Rsqr b - 4 * a * c = Delta a b c).
-intro;
- replace (- ((4 * a * c - Rsqr b) / (4 * a))) with
-  ((Rsqr b - 4 * a * c) / (4 * a)).
-rewrite H1; intro;
- generalize
-  (Rmult_eq_compat_l (/ a) (a * Rsqr (x + b / (2 * a)))
-     (Delta a b c / (4 * a)) H2);
- replace (/ a * (a * Rsqr (x + b / (2 * a)))) with (Rsqr (x + b / (2 * a))).
-replace (/ a * (Delta a b c / (4 * a))) with
- (Rsqr (sqrt (Delta a b c) / (2 * a))).
-intro;
- generalize (Rsqr_eq (x + b / (2 * a)) (sqrt (Delta a b c) / (2 * a)) H3);
- intro; elim H4; intro.
-left; unfold sol_x1 in |- *;
- generalize
-  (Rplus_eq_compat_l (- (b / (2 * a))) (x + b / (2 * a))
-     (sqrt (Delta a b c) / (2 * a)) H5);
- replace (- (b / (2 * a)) + (x + b / (2 * a))) with x.
-intro; rewrite H6; unfold Rdiv in |- *; ring.
-ring.
-right; unfold sol_x2 in |- *;
- generalize
-  (Rplus_eq_compat_l (- (b / (2 * a))) (x + b / (2 * a))
-     (- (sqrt (Delta a b c) / (2 * a))) H5);
- replace (- (b / (2 * a)) + (x + b / (2 * a))) with x.
-intro; rewrite H6; unfold Rdiv in |- *; ring.
-ring.
-rewrite Rsqr_div.
-rewrite Rsqr_sqrt.
-unfold Rdiv in |- *.
-repeat rewrite Rmult_assoc.
-rewrite (Rmult_comm (/ a)).
-rewrite Rmult_assoc.
-rewrite <- Rinv_mult_distr.
-replace (2 * (2 * a) * a) with (Rsqr (2 * a)).
-reflexivity.
-ring_Rsqr.
-rewrite <- Rmult_assoc; apply prod_neq_R0;
- [ discrR | apply (cond_nonzero a) ].
-apply (cond_nonzero a).
-assumption.
-apply prod_neq_R0; [ discrR | apply (cond_nonzero a) ].
-rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym.
-symmetry  in |- *; apply Rmult_1_l.
-apply (cond_nonzero a).
-unfold Rdiv in |- *; rewrite <- Ropp_mult_distr_l_reverse.
-rewrite Ropp_minus_distr.
-reflexivity.
-reflexivity.
+  forall (a:nonzeroreal) (b c x:R),
+    Delta_is_pos a b c ->
+    a * Rsqr x + b * x + c = 0 -> x = sol_x1 a b c \/ x = sol_x2 a b c.
+Proof.
+  intros; rewrite (canonical_Rsqr a b c x) in H0; rewrite Rplus_comm in H0;
+    generalize
+      (Rplus_opp_r_uniq ((4 * a * c - Rsqr b) / (4 * a))
+        (a * Rsqr (x + b / (2 * a))) H0); cut (Rsqr b - 4 * a * c = Delta a b c).
+  intro;
+    replace (- ((4 * a * c - Rsqr b) / (4 * a))) with
+    ((Rsqr b - 4 * a * c) / (4 * a)).
+  rewrite H1; intro;
+    generalize
+      (Rmult_eq_compat_l (/ a) (a * Rsqr (x + b / (2 * a)))
+        (Delta a b c / (4 * a)) H2);
+      replace (/ a * (a * Rsqr (x + b / (2 * a)))) with (Rsqr (x + b / (2 * a))).
+  replace (/ a * (Delta a b c / (4 * a))) with
+  (Rsqr (sqrt (Delta a b c) / (2 * a))).
+  intro;
+    generalize (Rsqr_eq (x + b / (2 * a)) (sqrt (Delta a b c) / (2 * a)) H3);
+      intro; elim H4; intro.
+  left; unfold sol_x1 in |- *;
+    generalize
+      (Rplus_eq_compat_l (- (b / (2 * a))) (x + b / (2 * a))
+        (sqrt (Delta a b c) / (2 * a)) H5);
+      replace (- (b / (2 * a)) + (x + b / (2 * a))) with x.
+  intro; rewrite H6; unfold Rdiv in |- *; ring.
+  ring.
+  right; unfold sol_x2 in |- *;
+    generalize
+      (Rplus_eq_compat_l (- (b / (2 * a))) (x + b / (2 * a))
+        (- (sqrt (Delta a b c) / (2 * a))) H5);
+      replace (- (b / (2 * a)) + (x + b / (2 * a))) with x.
+  intro; rewrite H6; unfold Rdiv in |- *; ring.
+  ring.
+  rewrite Rsqr_div.
+  rewrite Rsqr_sqrt.
+  unfold Rdiv in |- *.
+  repeat rewrite Rmult_assoc.
+  rewrite (Rmult_comm (/ a)).
+  rewrite Rmult_assoc.
+  rewrite <- Rinv_mult_distr.
+  replace (2 * (2 * a) * a) with (Rsqr (2 * a)).
+  reflexivity.
+  ring_Rsqr.
+  rewrite <- Rmult_assoc; apply prod_neq_R0;
+    [ discrR | apply (cond_nonzero a) ].
+  apply (cond_nonzero a).
+  assumption.
+  apply prod_neq_R0; [ discrR | apply (cond_nonzero a) ].
+  rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym.
+  symmetry  in |- *; apply Rmult_1_l.
+  apply (cond_nonzero a).
+  unfold Rdiv in |- *; rewrite <- Ropp_mult_distr_l_reverse.
+  rewrite Ropp_minus_distr.
+  reflexivity.
+  reflexivity.
 Qed.