Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 336 insertions, 188 deletions

diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v
index 759e4b164..f4d5ccf1a 100644
--- a/theories/Reals/R_sqrt.v
+++ b/theories/Reals/R_sqrt.v
@@ -8,244 +8,392 @@
 
 (*i $Id$ i*)
 
-Require Rbase.
-Require Rfunctions.
-Require Rsqrt_def.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+Require Import Rbase.
+Require Import Rfunctions.
+Require Import Rsqrt_def. Open Local Scope R_scope.
 
 (* Here is a continuous extension of Rsqrt on R *)
-Definition sqrt : R->R := [x:R](Cases (case_Rabsolu x) of
-      (leftT _) => R0
-    | (rightT a) => (Rsqrt (mknonnegreal x (Rle_sym2 ? ? a))) end).
-
-Lemma sqrt_positivity : (x:R) ``0<=x`` -> ``0<=(sqrt x)``.
-Intros.
-Unfold sqrt.
-Case (case_Rabsolu x); Intro.
-Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? r H)).
-Apply Rsqrt_positivity.
+Definition sqrt (x:R) : R :=
+  match Rcase_abs x with
+  | 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.
 Qed.
 
-Lemma sqrt_sqrt : (x:R) ``0<=x`` -> ``(sqrt x)*(sqrt x)==x``.
-Intros.
-Unfold sqrt.
-Case (case_Rabsolu x); Intro.
-Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? r H)).
-Rewrite Rsqrt_Rsqrt; Reflexivity.
+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.
 Qed.
 
-Lemma sqrt_0 : ``(sqrt 0)==0``.
-Apply Rsqr_eq_0; Unfold Rsqr; Apply sqrt_sqrt; Right; Reflexivity. 
+Lemma sqrt_0 : sqrt 0 = 0.
+apply Rsqr_eq_0; unfold Rsqr in |- *; apply sqrt_sqrt; right; reflexivity. 
 Qed.
 
-Lemma sqrt_1 : ``(sqrt 1)==1``.
-Apply (Rsqr_inj (sqrt R1) R1); [Apply sqrt_positivity; Left | Left | Unfold Rsqr; Rewrite -> sqrt_sqrt; [Ring | Left]]; Apply Rlt_R0_R1.
+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.
 Qed.
 
-Lemma sqrt_eq_0 : (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_O.
+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.
 Qed.
 
-Lemma sqrt_lem_0 : (x,y:R) ``0<=x``->``0<=y``->(sqrt x)==y->``y*y==x``.
-Intros; Rewrite <- H1; Apply (sqrt_sqrt x H).
+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).
 Qed.
 
-Lemma sqtr_lem_1 : (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; Rewrite -> H1; Apply (sqrt_sqrt x H)].
+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) ].
 Qed.
 
-Lemma sqrt_def : (x:R) ``0<=x``->``(sqrt x)*(sqrt x)==x``.
-Intros; Apply (sqrt_sqrt x H).
+Lemma sqrt_def : forall x:R, 0 <= x -> sqrt x * sqrt x = x.
+intros; apply (sqrt_sqrt x H).
 Qed.
 
-Lemma sqrt_square : (x:R) ``0<=x``->``(sqrt (x*x))==x``.
-Intros; Apply (Rsqr_inj (sqrt (Rsqr x)) x (sqrt_positivity (Rsqr x) (pos_Rsqr x)) H); Unfold Rsqr; Apply (sqrt_sqrt (Rsqr x) (pos_Rsqr x)).
+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)).
 Qed.
 
-Lemma sqrt_Rsqr : (x:R) ``0<=x``->``(sqrt (Rsqr x))==x``.
-Intros; Unfold Rsqr; Apply sqrt_square; Assumption.
+Lemma sqrt_Rsqr : forall x:R, 0 <= x -> sqrt (Rsqr x) = x.
+intros; unfold Rsqr in |- *; apply sqrt_square; assumption.
 Qed.
 
-Lemma sqrt_Rsqr_abs : (x:R) (sqrt (Rsqr x))==(Rabsolu x).
-Intro x; Rewrite -> Rsqr_abs; Apply sqrt_Rsqr; Apply Rabsolu_pos.
+Lemma sqrt_Rsqr_abs : forall x:R, sqrt (Rsqr x) = Rabs x.
+intro x; rewrite Rsqr_abs; apply sqrt_Rsqr; apply Rabs_pos.
 Qed.
 
-Lemma Rsqr_sqrt : (x:R) ``0<=x``->(Rsqr (sqrt x))==x.
-Intros x H1; Unfold Rsqr; Apply (sqrt_sqrt x H1).
+Lemma Rsqr_sqrt : forall x:R, 0 <= x -> Rsqr (sqrt x) = x.
+intros x H1; unfold Rsqr in |- *; apply (sqrt_sqrt x H1).
 Qed.
 
-Lemma sqrt_times : (x,y:R) ``0<=x``->``0<=y``->``(sqrt (x*y))==(sqrt x)*(sqrt y)``.
-Intros x y H1 H2; Apply (Rsqr_inj (sqrt (Rmult x y)) (Rmult (sqrt x) (sqrt y)) (sqrt_positivity (Rmult 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_times; Repeat Rewrite Rsqr_sqrt; [Ring | Assumption |Assumption | Apply (Rmult_le_pos x y H1 H2)].
+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) ].
 Qed.
 
-Lemma sqrt_lt_R0 : (x:R) ``0<x`` -> ``0<(sqrt x)``.
-Intros x H1; Apply Rsqr_incrst_0; [Rewrite Rsqr_O; Rewrite Rsqr_sqrt ; [Assumption | Left; Assumption] | Right; Reflexivity | Apply (sqrt_positivity x (Rlt_le R0 x H1))].
+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)) ].
 Qed.
 
-Lemma sqrt_div : (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 (Rinv y)); [ Assumption | Generalize (Rlt_Rinv y H2); Clear H2; Intro H2; Left; Assumption] | Apply (Rmult_le_pos (sqrt x) (Rinv (sqrt y))) ; [ Apply (sqrt_positivity x H1) | Generalize (sqrt_lt_R0 y H2); Clear H2; Intro H2; Generalize (Rlt_Rinv (sqrt y) H2); Clear H2; Intro H2; Left; Assumption] | Rewrite Rsqr_div; Repeat Rewrite Rsqr_sqrt; [ Reflexivity | Left; Assumption | Assumption | Generalize (Rlt_Rinv y H2); Intro H3; Generalize (Rlt_le R0 (Rinv y) H3); Intro H4; Apply (Rmult_le_pos x (Rinv y) H1 H4) |Red; Intro H3; Generalize (Rlt_le R0 y H2); Intro H4; Generalize (sqrt_eq_0 y H4 H3); Intro H5; Rewrite H5 in H2; Elim (Rlt_antirefl R0 H2)]].
+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) ] ].
 Qed.
 
-Lemma sqrt_lt_0 : (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.
+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.
 Qed.
 
-Lemma sqrt_lt_1 : (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)].
+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) ].
 Qed.
 
-Lemma sqrt_le_0 : (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.
+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.
 Qed.
 
-Lemma sqrt_le_1 : (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)].
+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) ].
 Qed.
 
-Lemma sqrt_inj : (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.
+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.
 Qed.
 
-Lemma sqrt_less : (x:R)  ``0<=x``->``1<x``->``(sqrt x)<x``.
-Intros x H1 H2; Generalize (sqrt_lt_1 R1 x (Rlt_le R0 R1 (Rlt_R0_R1)) H1 H2); Intro H3; Rewrite  sqrt_1 in H3; Generalize (Rmult_ne (sqrt x)); Intro H4; Elim H4; Intros H5 H6; Rewrite <- H5; Pattern 2 x; Rewrite <- (sqrt_def x H1); Apply (Rlt_monotony (sqrt x) R1 (sqrt x) (sqrt_lt_R0 x (Rlt_trans R0 R1 x Rlt_R0_R1 H2)) H3).
+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).
 Qed.
 
-Lemma sqrt_more : (x:R) ``0<x``->``x<1``->``x<(sqrt x)``.
-Intros x H1 H2; Generalize (sqrt_lt_1 x R1 (Rlt_le R0 x H1) (Rlt_le R0 R1 (Rlt_R0_R1)) H2); Intro H3; Rewrite  sqrt_1 in H3; Generalize (Rmult_ne (sqrt x)); Intro H4; Elim H4; Intros H5 H6; Rewrite <- H5; Pattern 1 x; Rewrite <- (sqrt_def x (Rlt_le R0 x H1)); Apply (Rlt_monotony (sqrt x) (sqrt x) R1 (sqrt_lt_R0 x H1) H3).
+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).
 Qed.
 
-Lemma sqrt_cauchy : (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_times; Repeat Rewrite Rsqr_sqrt; Unfold Rsqr; [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 Rle_compatibility; 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 1 ``2*a*b*c*d``; Rewrite <- Rplus_Or; Apply Rle_compatibility; Replace ``a*a*d*d+b*b*c*c-2*a*b*c*d`` with (Rsqr (Rminus (Rmult a d) (Rmult b c))); [Apply pos_Rsqr | Unfold Rsqr; Ring] | Ring] | Ring] | Ring] | Apply (ge0_plus_ge0_is_ge0 (Rsqr c) (Rsqr d) (pos_Rsqr c) (pos_Rsqr d)) | Apply (ge0_plus_ge0_is_ge0 (Rsqr a) (Rsqr b) (pos_Rsqr a) (pos_Rsqr b))] | Apply Rmult_le_pos; Apply sqrt_positivity; Apply ge0_plus_ge0_is_ge0; Apply pos_Rsqr].
+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
+          (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 - 2 * a * b * c * d)
+                 with (Rsqr (a * d - b * c));
+                [ apply Rle_0_sqr | unfold Rsqr in |- *; 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 ].
 Qed.
 
 (************************************************************)
 (* Resolution of [a*X^2+b*X+c=0]                            *)
 (************************************************************)
 
-Definition Delta [a:nonzeroreal;b,c:R] : R := ``(Rsqr b)-4*a*c``.
-
-Definition Delta_is_pos [a:nonzeroreal;b,c:R] : Prop := ``0<=(Delta a b c)``.
-
-Definition sol_x1 [a:nonzeroreal;b,c:R] : R := ``(-b+(sqrt (Delta a b c)))/(2*a)``.
-
-Definition sol_x2 [a:nonzeroreal;b,c:R] : R := ``(-b-(sqrt (Delta a b c)))/(2*a)``.
-
-Lemma Rsqr_sol_eq_0_1 : (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; Repeat Rewrite Rsqr_times; Rewrite Rsqr_plus; Rewrite <- Rsqr_neg; Rewrite Rsqr_sqrt.
-Rewrite Rsqr_inv.
-Unfold Rsqr; Repeat Rewrite Rinv_Rmult.
-Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym a).
-Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r; Rewrite Rmult_Rplus_distrl.
-Repeat Rewrite Rmult_assoc.
-Pattern 2 ``2``; Rewrite (Rmult_sym ``2``).
-Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r.
-Rewrite (Rmult_Rplus_distrl ``-b`` ``(sqrt (b*b-(2*(2*(a*c)))))`` ``(/2*/a)``).
-Rewrite Rmult_Rplus_distr; 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; Repeat Rewrite <- Rplus_assoc.
-Replace ``b*b+b*b`` with ``2*(b*b)``.
-Rewrite Rmult_Rplus_distrl; Repeat Rewrite Rmult_assoc.
-Rewrite (Rmult_sym ``2``); Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r.
-Rewrite Ropp_mul1; Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym ``2``).
-Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r; Rewrite (Rmult_sym ``/2``); Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym ``2``).
-Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r; Repeat Rewrite Rmult_assoc.
-Rewrite (Rmult_sym a); Rewrite Rmult_assoc.
-Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r; Rewrite <- Ropp_mul2.
-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; Repeat Rewrite Rsqr_times; Rewrite Rsqr_minus; Rewrite <- Rsqr_neg; Rewrite Rsqr_sqrt.
-Rewrite Rsqr_inv.
-Unfold Rsqr; Repeat Rewrite Rinv_Rmult; Repeat Rewrite Rmult_assoc.
-Rewrite (Rmult_sym a); Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r; Unfold Rminus; Rewrite Rmult_Rplus_distrl.
-Rewrite Ropp_mul1; Repeat Rewrite Rmult_assoc; Pattern 2 ``2``; Rewrite (Rmult_sym ``2``).
-Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r; Rewrite (Rmult_Rplus_distrl ``-b`` ``-(sqrt (b*b+ -(2*(2*(a*c))))) `` ``(/2*/a)``).
-Rewrite Rmult_Rplus_distr; Repeat Rewrite Rplus_assoc.
-Rewrite Ropp_mul1; Rewrite Ropp_Ropp.
-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_Rplus_distrl; Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym ``2``); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
-Rewrite Ropp_mul1; Repeat Rewrite Rmult_assoc.
-Rewrite (Rmult_sym ``2``); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r; Rewrite (Rmult_sym ``/2``); Repeat Rewrite Rmult_assoc.
-Rewrite (Rmult_sym ``2``); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r; Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym a); Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r; Rewrite <- Ropp_mul2; 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 Orelse Apply (cond_nonzero a).
-Apply prod_neq_R0; DiscrR Orelse Apply (cond_nonzero a).
-Apply prod_neq_R0; DiscrR Orelse Apply (cond_nonzero a).
-Assumption.
-Qed.
-
-Lemma Rsqr_sol_eq_0_0 : (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_sym in H0; Generalize (Rplus_Ropp  ``(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_mult_r ``/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; Generalize (Rplus_plus_r ``-(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; Ring.
-Ring.
-Right; Unfold sol_x2; Generalize (Rplus_plus_r ``-(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; Ring.
-Ring.
-Rewrite Rsqr_div.
-Rewrite Rsqr_sqrt.
-Unfold Rdiv.
-Repeat Rewrite Rmult_assoc.
-Rewrite (Rmult_sym ``/a``).
-Rewrite Rmult_assoc.
-Rewrite <- Rinv_Rmult.
-Replace ``(2*(2*a))*a`` with ``(Rsqr (2*a))``.
-Reflexivity.
-SqRing.
-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; Apply Rmult_1l.
-Apply (cond_nonzero a).
-Unfold Rdiv; Rewrite <- Ropp_mul1.
-Rewrite Ropp_distr2.
-Reflexivity.
-Reflexivity.
+Definition Delta (a:nonzeroreal) (b c:R) : R := Rsqr b - 4 * a * c.
+
+Definition Delta_is_pos (a:nonzeroreal) (b c:R) : Prop := 0 <= Delta a b c.
+
+Definition sol_x1 (a:nonzeroreal) (b c:R) : R :=
+  (- b + sqrt (Delta a b c)) / (2 * a).
+
+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.
 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.
+Qed.
\ No newline at end of file