Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import Rbase.
Require Import Rfunctions.
Require Import Rsqrt_def.
Local Open Scope R_scope.

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))
  end.

Lemma sqrt_pos : forall x : R, 0 <= sqrt x.forall x : R, 0 <= sqrt x
Proof.forall x : R, 0 <= sqrt x
  intros x.x:R
0 <= sqrt x
  unfold sqrt.x:R
0 <=
match Rcase_abs x with
| left _ => 0
| right a =>
    Rsqrt
      {| nonneg := x; cond_nonneg := Rge_le x 0 a |}
end
  destruct (Rcase_abs x) as [H|H].x:R
H:x < 0
0 <= 0
x:R
H:x >= 0
0 <=
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 H |}
  apply Rle_refl.x:R
H:x >= 0
0 <=
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 H |}
  apply Rsqrt_positivity.
Qed.

Lemma sqrt_positivity : forall x:R, 0 <= x -> 0 <= sqrt x.forall x : R, 0 <= x -> 0 <= sqrt x
Proof.forall x : R, 0 <= x -> 0 <= sqrt x
  intros x _.x:R
0 <= sqrt x
  apply sqrt_pos.
Qed.

Lemma sqrt_sqrt : forall x:R, 0 <= x -> sqrt x * sqrt x = x.forall x : R, 0 <= x -> sqrt x * sqrt x = x
Proof.forall x : R, 0 <= x -> sqrt x * sqrt x = x
  intros.x:R
H:0 <= x
sqrt x * sqrt x = x
  unfold sqrt.x:R
H:0 <= x
match Rcase_abs x with
| left _ => 0
| right a =>
    Rsqrt
      {| nonneg := x; cond_nonneg := Rge_le x 0 a |}
end *
match Rcase_abs x with
| left _ => 0
| right a =>
    Rsqrt
      {| nonneg := x; cond_nonneg := Rge_le x 0 a |}
end = x
  case (Rcase_abs x) as [Hlt|Hge].x:R
H:0 <= x
Hlt:x < 0
0 * 0 = x
x:R
H:0 <= x
Hge:x >= 0
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hge |} *
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hge |} =
x
  elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ Hlt H)).x:R
H:0 <= x
Hge:x >= 0
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hge |} *
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hge |} =
x
  rewrite Rsqrt_Rsqrt; reflexivity.
Qed.

Lemma sqrt_0 : sqrt 0 = 0.sqrt 0 = 0
Proof.sqrt 0 = 0
  apply Rsqr_eq_0; unfold Rsqr; apply sqrt_sqrt; right; reflexivity.
Qed.

Lemma sqrt_1 : sqrt 1 = 1.sqrt 1 = 1
Proof.sqrt 1 = 1
  apply (Rsqr_inj (sqrt 1) 1);
    [ apply sqrt_positivity; left
      | left
      | unfold Rsqr; rewrite sqrt_sqrt; [ ring | left ] ];
    apply Rlt_0_1.
Qed.

Lemma sqrt_eq_0 : forall x:R, 0 <= x -> sqrt x = 0 -> x = 0.forall x : R, 0 <= x -> sqrt x = 0 -> x = 0
Proof.forall x : R, 0 <= x -> sqrt x = 0 -> x = 0
  intros; cut (Rsqr (sqrt x) = 0).x:R
H:0 <= x
H0:sqrt x = 0
(sqrt x)² = 0 -> x = 0
x:R
H:0 <= x
H0:sqrt x = 0
(sqrt x)² = 0
  intro; unfold Rsqr in H1; rewrite sqrt_sqrt in H1; assumption.x:R
H:0 <= x
H0:sqrt x = 0
(sqrt x)² = 0
  rewrite H0; apply Rsqr_0.
Qed.

Lemma sqrt_lem_0 : forall x y:R, 0 <= x -> 0 <= y -> sqrt x = y -> y * y = x.forall x y : R,
0 <= x -> 0 <= y -> sqrt x = y -> y * y = x
Proof.forall x y : R,
0 <= x -> 0 <= y -> sqrt x = y -> y * y = x
  intros; rewrite <- H1; apply (sqrt_sqrt x H).
Qed.

Lemma sqrt_lem_1 : forall x y:R, 0 <= x -> 0 <= y -> y * y = x -> sqrt x = y.forall x y : R,
0 <= x -> 0 <= y -> y * y = x -> sqrt x = y
Proof.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; rewrite H1; apply (sqrt_sqrt x H) ].
Qed.

Lemma sqrt_def : forall x:R, 0 <= x -> sqrt x * sqrt x = x.forall x : R, 0 <= x -> sqrt x * sqrt x = x
Proof.forall x : R, 0 <= x -> sqrt x * sqrt x = x
  intros; apply (sqrt_sqrt x H).
Qed.

Lemma sqrt_square : forall x:R, 0 <= x -> sqrt (x * x) = x.forall x : R, 0 <= x -> sqrt (x * x) = x
Proof.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; apply (sqrt_sqrt (Rsqr x) (Rle_0_sqr x)).
Qed.

Lemma sqrt_Rsqr : forall x:R, 0 <= x -> sqrt (Rsqr x) = x.forall x : R, 0 <= x -> sqrt x² = x
Proof.forall x : R, 0 <= x -> sqrt x² = x
  intros; unfold Rsqr; apply sqrt_square; assumption.
Qed.

Lemma sqrt_pow2 : forall x, 0 <= x -> sqrt (x ^ 2) = x.forall x : R, 0 <= x -> sqrt (x ^ 2) = x
intros; simpl; rewrite Rmult_1_r, sqrt_square; auto.
Qed.

Lemma sqrt_Rsqr_abs : forall x:R, sqrt (Rsqr x) = Rabs x.forall x : R, sqrt x² = Rabs x
Proof.forall x : R, sqrt x² = Rabs x
  intro x; rewrite Rsqr_abs; apply sqrt_Rsqr; apply Rabs_pos.
Qed.

Lemma Rsqr_sqrt : forall x:R, 0 <= x -> Rsqr (sqrt x) = x.forall x : R, 0 <= x -> (sqrt x)² = x
Proof.forall x : R, 0 <= x -> (sqrt x)² = x
  intros x H1; unfold Rsqr; apply (sqrt_sqrt x H1).
Qed.

Lemma sqrt_mult_alt :
  forall x y : R, 0 <= x -> sqrt (x * y) = sqrt x * sqrt y.forall x y : R,
0 <= x -> sqrt (x * y) = sqrt x * sqrt y
Proof.forall x y : R,
0 <= x -> sqrt (x * y) = sqrt x * sqrt y
  intros x y Hx.x, y:R
Hx:0 <= x
sqrt (x * y) = sqrt x * sqrt y
  unfold sqrt at 3.x, y:R
Hx:0 <= x
sqrt (x * y) =
sqrt x *
match Rcase_abs y with
| left _ => 0
| right a =>
    Rsqrt
      {| nonneg := y; cond_nonneg := Rge_le y 0 a |}
end
  destruct (Rcase_abs y) as [Hy|Hy].x, y:R
Hx:0 <= x
Hy:y < 0
sqrt (x * y) = sqrt x * 0
x, y:R
Hx:0 <= x
Hy:y >= 0
sqrt (x * y) =
sqrt x *
Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |}
  rewrite Rmult_0_r.x, y:R
Hx:0 <= x
Hy:y < 0
sqrt (x * y) = 0
x, y:R
Hx:0 <= x
Hy:y >= 0
sqrt (x * y) =
sqrt x *
Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |}
  destruct Hx as [Hx'|Hx'].x, y:R
Hx':0 < x
Hy:y < 0
sqrt (x * y) = 0
x, y:R
Hx':0 = x
Hy:y < 0
sqrt (x * y) = 0
x, y:R
Hx:0 <= x
Hy:y >= 0
sqrt (x * y) =
sqrt x *
Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |}
  unfold sqrt.x, y:R
Hx':0 < x
Hy:y < 0
match Rcase_abs (x * y) with
| left _ => 0
| right a =>
    Rsqrt
      {|
      nonneg := x * y;
      cond_nonneg := Rge_le (x * y) 0 a |}
end = 0
x, y:R
Hx':0 = x
Hy:y < 0
sqrt (x * y) = 0
x, y:R
Hx:0 <= x
Hy:y >= 0
sqrt (x * y) =
sqrt x *
Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |}
  destruct (Rcase_abs (x * y)) as [Hxy|Hxy].x, y:R
Hx':0 < x
Hy:y < 0
Hxy:x * y < 0
0 = 0
x, y:R
Hx':0 < x
Hy:y < 0
Hxy:x * y >= 0
Rsqrt
  {|
  nonneg := x * y;
  cond_nonneg := Rge_le (x * y) 0 Hxy |} = 0
x, y:R
Hx':0 = x
Hy:y < 0
sqrt (x * y) = 0
x, y:R
Hx:0 <= x
Hy:y >= 0
sqrt (x * y) =
sqrt x *
Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |}
  apply eq_refl.x, y:R
Hx':0 < x
Hy:y < 0
Hxy:x * y >= 0
Rsqrt
  {|
  nonneg := x * y;
  cond_nonneg := Rge_le (x * y) 0 Hxy |} = 0
x, y:R
Hx':0 = x
Hy:y < 0
sqrt (x * y) = 0
x, y:R
Hx:0 <= x
Hy:y >= 0
sqrt (x * y) =
sqrt x *
Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |}
  elim Rge_not_lt with (1 := Hxy).x, y:R
Hx':0 < x
Hy:y < 0
Hxy:x * y >= 0
x * y < 0
x, y:R
Hx':0 = x
Hy:y < 0
sqrt (x * y) = 0
x, y:R
Hx:0 <= x
Hy:y >= 0
sqrt (x * y) =
sqrt x *
Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |}
  rewrite <- (Rmult_0_r x).x, y:R
Hx':0 < x
Hy:y < 0
Hxy:x * y >= 0
x * y < x * 0
x, y:R
Hx':0 = x
Hy:y < 0
sqrt (x * y) = 0
x, y:R
Hx:0 <= x
Hy:y >= 0
sqrt (x * y) =
sqrt x *
Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |}
  now apply Rmult_lt_compat_l.x, y:R
Hx':0 = x
Hy:y < 0
sqrt (x * y) = 0
x, y:R
Hx:0 <= x
Hy:y >= 0
sqrt (x * y) =
sqrt x *
Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |}
  rewrite <- Hx', Rmult_0_l.x, y:R
Hx':0 = x
Hy:y < 0
sqrt 0 = 0
x, y:R
Hx:0 <= x
Hy:y >= 0
sqrt (x * y) =
sqrt x *
Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |}
  exact sqrt_0.x, y:R
Hx:0 <= x
Hy:y >= 0
sqrt (x * y) =
sqrt x *
Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |}
  apply Rsqr_inj.x, y:R
Hx:0 <= x
Hy:y >= 0
0 <= sqrt (x * y)
x, y:R
Hx:0 <= x
Hy:y >= 0
0 <=
sqrt x *
Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |}
x, y:R
Hx:0 <= x
Hy:y >= 0
(sqrt (x * y))² =
(sqrt x *
 Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |})²
  apply sqrt_pos.x, y:R
Hx:0 <= x
Hy:y >= 0
0 <=
sqrt x *
Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |}
x, y:R
Hx:0 <= x
Hy:y >= 0
(sqrt (x * y))² =
(sqrt x *
 Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |})²
  apply Rmult_le_pos.x, y:R
Hx:0 <= x
Hy:y >= 0
0 <= sqrt x
x, y:R
Hx:0 <= x
Hy:y >= 0
0 <=
Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |}
x, y:R
Hx:0 <= x
Hy:y >= 0
(sqrt (x * y))² =
(sqrt x *
 Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |})²
  apply sqrt_pos.x, y:R
Hx:0 <= x
Hy:y >= 0
0 <=
Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |}
x, y:R
Hx:0 <= x
Hy:y >= 0
(sqrt (x * y))² =
(sqrt x *
 Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |})²
  apply Rsqrt_positivity.x, y:R
Hx:0 <= x
Hy:y >= 0
(sqrt (x * y))² =
(sqrt x *
 Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |})²
  rewrite Rsqr_mult, 2!Rsqr_sqrt.x, y:R
Hx:0 <= x
Hy:y >= 0
x * y =
x *
(Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |})²
x, y:R
Hx:0 <= x
Hy:y >= 0
0 <= x
x, y:R
Hx:0 <= x
Hy:y >= 0
0 <= x * y
  unfold Rsqr.x, y:R
Hx:0 <= x
Hy:y >= 0
x * y =
x *
(Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |} *
 Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |})
x, y:R
Hx:0 <= x
Hy:y >= 0
0 <= x
x, y:R
Hx:0 <= x
Hy:y >= 0
0 <= x * y
  now rewrite Rsqrt_Rsqrt.x, y:R
Hx:0 <= x
Hy:y >= 0
0 <= x
x, y:R
Hx:0 <= x
Hy:y >= 0
0 <= x * y
  exact Hx.x, y:R
Hx:0 <= x
Hy:y >= 0
0 <= x * y
  apply Rmult_le_pos.x, y:R
Hx:0 <= x
Hy:y >= 0
0 <= x
x, y:R
Hx:0 <= x
Hy:y >= 0
0 <= y
  exact Hx.x, y:R
Hx:0 <= x
Hy:y >= 0
0 <= y
  now apply Rge_le.
Qed.

Lemma sqrt_mult :
  forall x y:R, 0 <= x -> 0 <= y -> sqrt (x * y) = sqrt x * sqrt y.forall x y : R,
0 <= x -> 0 <= y -> sqrt (x * y) = sqrt x * sqrt y
Proof.forall x y : R,
0 <= x -> 0 <= y -> sqrt (x * y) = sqrt x * sqrt y
  intros x y Hx _.x, y:R
Hx:0 <= x
sqrt (x * y) = sqrt x * sqrt y
  now apply sqrt_mult_alt.
Qed.

Lemma sqrt_lt_R0 : forall x:R, 0 < x -> 0 < sqrt x.forall x : R, 0 < x -> 0 < sqrt x
Proof.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 Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y.forall x y : R, 0 < x -> 0 < y -> 0 < x * / y
intros x y H H0; try assumption.x, y:R
H:0 < x
H0:0 < y
0 < x * / y
replace 0 with (x * 0).x, y:R
H:0 < x
H0:0 < y
x * 0 < x * / y
x, y:R
H:0 < x
H0:0 < y
x * 0 = 0
apply Rmult_lt_compat_l; auto with real.x, y:R
H:0 < x
H0:0 < y
x * 0 = 0
ring.
Qed.

Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y.forall x y : R, 0 <= x -> 0 < y -> 0 <= x * / y
intros x y H H0; try assumption.x, y:R
H:0 <= x
H0:0 < y
0 <= x * / y
case H; intros.x, y:R
H:0 <= x
H0:0 < y
H1:0 < x
0 <= x * / y
x, y:R
H:0 <= x
H0:0 < y
H1:0 = x
0 <= x * / y
red; left.x, y:R
H:0 <= x
H0:0 < y
H1:0 < x
0 < x * / y
x, y:R
H:0 <= x
H0:0 < y
H1:0 = x
0 <= x * / y
apply Rlt_mult_inv_pos; auto with real.x, y:R
H:0 <= x
H0:0 < y
H1:0 = x
0 <= x * / y
rewrite <- H1.x, y:R
H:0 <= x
H0:0 < y
H1:0 = x
0 <= 0 * / y
red; right; ring.
Qed.

Lemma sqrt_div_alt :
  forall x y : R, 0 < y -> sqrt (x / y) = sqrt x / sqrt y.forall x y : R,
0 < y -> sqrt (x / y) = sqrt x / sqrt y
Proof.forall x y : R,
0 < y -> sqrt (x / y) = sqrt x / sqrt y
  intros x y Hy.x, y:R
Hy:0 < y
sqrt (x / y) = sqrt x / sqrt y
  unfold sqrt at 2.x, y:R
Hy:0 < y
sqrt (x / y) =
match Rcase_abs x with
| left _ => 0
| right a =>
    Rsqrt
      {| nonneg := x; cond_nonneg := Rge_le x 0 a |}
end / sqrt y
  destruct (Rcase_abs x) as [Hx|Hx].x, y:R
Hy:0 < y
Hx:x < 0
sqrt (x / y) = 0 / sqrt y
x, y:R
Hy:0 < y
Hx:x >= 0
sqrt (x / y) =
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hx |} /
sqrt y
  unfold Rdiv.x, y:R
Hy:0 < y
Hx:x < 0
sqrt (x * / y) = 0 * / sqrt y
x, y:R
Hy:0 < y
Hx:x >= 0
sqrt (x / y) =
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hx |} /
sqrt y
  rewrite Rmult_0_l.x, y:R
Hy:0 < y
Hx:x < 0
sqrt (x * / y) = 0
x, y:R
Hy:0 < y
Hx:x >= 0
sqrt (x / y) =
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hx |} /
sqrt y
  unfold sqrt.x, y:R
Hy:0 < y
Hx:x < 0
match Rcase_abs (x * / y) with
| left _ => 0
| right a =>
    Rsqrt
      {|
      nonneg := x * / y;
      cond_nonneg := Rge_le (x * / y) 0 a |}
end = 0
x, y:R
Hy:0 < y
Hx:x >= 0
sqrt (x / y) =
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hx |} /
sqrt y
  destruct (Rcase_abs (x * / y)) as [Hxy|Hxy].x, y:R
Hy:0 < y
Hx:x < 0
Hxy:x * / y < 0
0 = 0
x, y:R
Hy:0 < y
Hx:x < 0
Hxy:x * / y >= 0
Rsqrt
  {|
  nonneg := x * / y;
  cond_nonneg := Rge_le (x * / y) 0 Hxy |} = 0
x, y:R
Hy:0 < y
Hx:x >= 0
sqrt (x / y) =
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hx |} /
sqrt y
  apply eq_refl.x, y:R
Hy:0 < y
Hx:x < 0
Hxy:x * / y >= 0
Rsqrt
  {|
  nonneg := x * / y;
  cond_nonneg := Rge_le (x * / y) 0 Hxy |} = 0
x, y:R
Hy:0 < y
Hx:x >= 0
sqrt (x / y) =
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hx |} /
sqrt y
  elim Rge_not_lt with (1 := Hxy).x, y:R
Hy:0 < y
Hx:x < 0
Hxy:x * / y >= 0
x * / y < 0
x, y:R
Hy:0 < y
Hx:x >= 0
sqrt (x / y) =
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hx |} /
sqrt y
  apply Rmult_lt_reg_r with y.x, y:R
Hy:0 < y
Hx:x < 0
Hxy:x * / y >= 0
0 < y
x, y:R
Hy:0 < y
Hx:x < 0
Hxy:x * / y >= 0
x * / y * y < 0 * y
x, y:R
Hy:0 < y
Hx:x >= 0
sqrt (x / y) =
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hx |} /
sqrt y
  exact Hy.x, y:R
Hy:0 < y
Hx:x < 0
Hxy:x * / y >= 0
x * / y * y < 0 * y
x, y:R
Hy:0 < y
Hx:x >= 0
sqrt (x / y) =
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hx |} /
sqrt y
  rewrite Rmult_assoc, Rinv_l, Rmult_1_r, Rmult_0_l.x, y:R
Hy:0 < y
Hx:x < 0
Hxy:x * / y >= 0
x < 0
x, y:R
Hy:0 < y
Hx:x < 0
Hxy:x * / y >= 0
y <> 0
x, y:R
Hy:0 < y
Hx:x >= 0
sqrt (x / y) =
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hx |} /
sqrt y
  exact Hx.x, y:R
Hy:0 < y
Hx:x < 0
Hxy:x * / y >= 0
y <> 0
x, y:R
Hy:0 < y
Hx:x >= 0
sqrt (x / y) =
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hx |} /
sqrt y
  now apply Rgt_not_eq.x, y:R
Hy:0 < y
Hx:x >= 0
sqrt (x / y) =
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hx |} /
sqrt y
  set (Hx' := Rge_le x 0 Hx).x, y:R
Hy:0 < y
Hx:x >= 0
Hx':=Rge_le x 0 Hx:0 <= x
sqrt (x / y) =
Rsqrt {| nonneg := x; cond_nonneg := Hx' |} / sqrt y
  clearbody Hx'.x, y:R
Hy:0 < y
Hx:x >= 0
Hx':0 <= x
sqrt (x / y) =
Rsqrt {| nonneg := x; cond_nonneg := Hx' |} / sqrt y clear Hx.x, y:R
Hy:0 < y
Hx':0 <= x
sqrt (x / y) =
Rsqrt {| nonneg := x; cond_nonneg := Hx' |} / sqrt y
  apply Rsqr_inj.x, y:R
Hy:0 < y
Hx':0 <= x
0 <= sqrt (x / y)
x, y:R
Hy:0 < y
Hx':0 <= x
0 <=
Rsqrt {| nonneg := x; cond_nonneg := Hx' |} / sqrt y
x, y:R
Hy:0 < y
Hx':0 <= x
(sqrt (x / y))² =
(Rsqrt {| nonneg := x; cond_nonneg := Hx' |} / sqrt y)²
  apply sqrt_pos.x, y:R
Hy:0 < y
Hx':0 <= x
0 <=
Rsqrt {| nonneg := x; cond_nonneg := Hx' |} / sqrt y
x, y:R
Hy:0 < y
Hx':0 <= x
(sqrt (x / y))² =
(Rsqrt {| nonneg := x; cond_nonneg := Hx' |} / sqrt y)²
  apply Rle_mult_inv_pos.x, y:R
Hy:0 < y
Hx':0 <= x
0 <= Rsqrt {| nonneg := x; cond_nonneg := Hx' |}
x, y:R
Hy:0 < y
Hx':0 <= x
0 < sqrt y
x, y:R
Hy:0 < y
Hx':0 <= x
(sqrt (x / y))² =
(Rsqrt {| nonneg := x; cond_nonneg := Hx' |} / sqrt y)²
  apply Rsqrt_positivity.x, y:R
Hy:0 < y
Hx':0 <= x
0 < sqrt y
x, y:R
Hy:0 < y
Hx':0 <= x
(sqrt (x / y))² =
(Rsqrt {| nonneg := x; cond_nonneg := Hx' |} / sqrt y)²
  now apply sqrt_lt_R0.x, y:R
Hy:0 < y
Hx':0 <= x
(sqrt (x / y))² =
(Rsqrt {| nonneg := x; cond_nonneg := Hx' |} / sqrt y)²
  rewrite Rsqr_div, 2!Rsqr_sqrt.x, y:R
Hy:0 < y
Hx':0 <= x
x / y =
(Rsqrt {| nonneg := x; cond_nonneg := Hx' |})² / y
x, y:R
Hy:0 < y
Hx':0 <= x
0 <= y
x, y:R
Hy:0 < y
Hx':0 <= x
0 <= x / y
x, y:R
Hy:0 < y
Hx':0 <= x
sqrt y <> 0
  unfold Rsqr.x, y:R
Hy:0 < y
Hx':0 <= x
x / y =
Rsqrt {| nonneg := x; cond_nonneg := Hx' |} *
Rsqrt {| nonneg := x; cond_nonneg := Hx' |} / y
x, y:R
Hy:0 < y
Hx':0 <= x
0 <= y
x, y:R
Hy:0 < y
Hx':0 <= x
0 <= x / y
x, y:R
Hy:0 < y
Hx':0 <= x
sqrt y <> 0
  now rewrite Rsqrt_Rsqrt.x, y:R
Hy:0 < y
Hx':0 <= x
0 <= y
x, y:R
Hy:0 < y
Hx':0 <= x
0 <= x / y
x, y:R
Hy:0 < y
Hx':0 <= x
sqrt y <> 0
  now apply Rlt_le.x, y:R
Hy:0 < y
Hx':0 <= x
0 <= x / y
x, y:R
Hy:0 < y
Hx':0 <= x
sqrt y <> 0
  now apply Rle_mult_inv_pos.x, y:R
Hy:0 < y
Hx':0 <= x
sqrt y <> 0
  apply Rgt_not_eq.x, y:R
Hy:0 < y
Hx':0 <= x
sqrt y > 0
  now apply sqrt_lt_R0.
Qed.

Lemma sqrt_div :
  forall x y:R, 0 <= x -> 0 < y -> sqrt (x / y) = sqrt x / sqrt y.forall x y : R,
0 <= x -> 0 < y -> sqrt (x / y) = sqrt x / sqrt y
Proof.forall x y : R,
0 <= x -> 0 < y -> sqrt (x / y) = sqrt x / sqrt y
  intros x y _ H.x, y:R
H:0 < y
sqrt (x / y) = sqrt x / sqrt y
  now apply sqrt_div_alt.
Qed.

Lemma sqrt_lt_0_alt :
  forall x y : R, sqrt x < sqrt y -> x < y.forall x y : R, sqrt x < sqrt y -> x < y
Proof.forall x y : R, sqrt x < sqrt y -> x < y
  intros x y.x, y:R
sqrt x < sqrt y -> x < y
  unfold sqrt at 2.x, y:R
sqrt x <
match Rcase_abs y with
| left _ => 0
| right a =>
    Rsqrt
      {| nonneg := y; cond_nonneg := Rge_le y 0 a |}
end -> x < y
  destruct (Rcase_abs y) as [Hy|Hy].x, y:R
Hy:y < 0
sqrt x < 0 -> x < y
x, y:R
Hy:y >= 0
sqrt x <
Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |} ->
x < y
  intros Hx.x, y:R
Hy:y < 0
Hx:sqrt x < 0
x < y
x, y:R
Hy:y >= 0
sqrt x <
Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |} ->
x < y
  elim Rlt_not_le with (1 := Hx).x, y:R
Hy:y < 0
Hx:sqrt x < 0
0 <= sqrt x
x, y:R
Hy:y >= 0
sqrt x <
Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |} ->
x < y
  apply sqrt_pos.x, y:R
Hy:y >= 0
sqrt x <
Rsqrt {| nonneg := y; cond_nonneg := Rge_le y 0 Hy |} ->
x < y
  set (Hy' := Rge_le y 0 Hy).x, y:R
Hy:y >= 0
Hy':=Rge_le y 0 Hy:0 <= y
sqrt x < Rsqrt {| nonneg := y; cond_nonneg := Hy' |} ->
x < y
  clearbody Hy'.x, y:R
Hy:y >= 0
Hy':0 <= y
sqrt x < Rsqrt {| nonneg := y; cond_nonneg := Hy' |} ->
x < y clear Hy.x, y:R
Hy':0 <= y
sqrt x < Rsqrt {| nonneg := y; cond_nonneg := Hy' |} ->
x < y
  unfold sqrt.x, y:R
Hy':0 <= y
match Rcase_abs x with
| left _ => 0
| right a =>
    Rsqrt
      {| nonneg := x; cond_nonneg := Rge_le x 0 a |}
end < Rsqrt {| nonneg := y; cond_nonneg := Hy' |} ->
x < y
  destruct (Rcase_abs x) as [Hx|Hx].x, y:R
Hy':0 <= y
Hx:x < 0
0 < Rsqrt {| nonneg := y; cond_nonneg := Hy' |} ->
x < y
x, y:R
Hy':0 <= y
Hx:x >= 0
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hx |} <
Rsqrt {| nonneg := y; cond_nonneg := Hy' |} -> x < y
  intros _.x, y:R
Hy':0 <= y
Hx:x < 0
x < y
x, y:R
Hy':0 <= y
Hx:x >= 0
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hx |} <
Rsqrt {| nonneg := y; cond_nonneg := Hy' |} -> x < y
  now apply Rlt_le_trans with R0.x, y:R
Hy':0 <= y
Hx:x >= 0
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hx |} <
Rsqrt {| nonneg := y; cond_nonneg := Hy' |} -> x < y
  intros Hxy.x, y:R
Hy':0 <= y
Hx:x >= 0
Hxy:Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hx |} <
Rsqrt {| nonneg := y; cond_nonneg := Hy' |}
x < y
  apply Rsqr_incrst_1 in Hxy ; try apply Rsqrt_positivity.x, y:R
Hy':0 <= y
Hx:x >= 0
Hxy:(Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hx |})² <
(Rsqrt {| nonneg := y; cond_nonneg := Hy' |})²
x < y
  unfold Rsqr in Hxy.x, y:R
Hy':0 <= y
Hx:x >= 0
Hxy:Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hx |} *
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hx |} <
Rsqrt {| nonneg := y; cond_nonneg := Hy' |} *
Rsqrt {| nonneg := y; cond_nonneg := Hy' |}
x < y
  now rewrite 2!Rsqrt_Rsqrt in Hxy.
Qed.

Lemma sqrt_lt_0 : forall x y:R, 0 <= x -> 0 <= y -> sqrt x < sqrt y -> x < y.forall x y : R,
0 <= x -> 0 <= y -> sqrt x < sqrt y -> x < y
Proof.forall x y : R,
0 <= x -> 0 <= y -> sqrt x < sqrt y -> x < y
  intros x y _ _.x, y:R
sqrt x < sqrt y -> x < y
  apply sqrt_lt_0_alt.
Qed.

Lemma sqrt_lt_1_alt :
  forall x y : R, 0 <= x < y -> sqrt x < sqrt y.forall x y : R, 0 <= x < y -> sqrt x < sqrt y
Proof.forall x y : R, 0 <= x < y -> sqrt x < sqrt y
  intros x y (Hx, Hxy).x, y:R
Hx:0 <= x
Hxy:x < y
sqrt x < sqrt y
  apply Rsqr_incrst_0 ; try apply sqrt_pos.x, y:R
Hx:0 <= x
Hxy:x < y
(sqrt x)² < (sqrt y)²
  rewrite 2!Rsqr_sqrt.x, y:R
Hx:0 <= x
Hxy:x < y
x < y
x, y:R
Hx:0 <= x
Hxy:x < y
0 <= y
x, y:R
Hx:0 <= x
Hxy:x < y
0 <= x
  exact Hxy.x, y:R
Hx:0 <= x
Hxy:x < y
0 <= y
x, y:R
Hx:0 <= x
Hxy:x < y
0 <= x
  apply Rlt_le.x, y:R
Hx:0 <= x
Hxy:x < y
0 < y
x, y:R
Hx:0 <= x
Hxy:x < y
0 <= x
  now apply Rle_lt_trans with x.x, y:R
Hx:0 <= x
Hxy:x < y
0 <= x
  exact Hx.
Qed.

Lemma sqrt_lt_1 : forall x y:R, 0 <= x -> 0 <= y -> x < y -> sqrt x < sqrt y.forall x y : R,
0 <= x -> 0 <= y -> x < y -> sqrt x < sqrt y
Proof.forall x y : R,
0 <= x -> 0 <= y -> x < y -> sqrt x < sqrt y
  intros x y Hx _ Hxy.x, y:R
Hx:0 <= x
Hxy:x < y
sqrt x < sqrt y
  apply sqrt_lt_1_alt.x, y:R
Hx:0 <= x
Hxy:x < y
0 <= x < y
  now split.
Qed.

Lemma sqrt_le_0 :
  forall x y:R, 0 <= x -> 0 <= y -> sqrt x <= sqrt y -> x <= y.forall x y : R,
0 <= x -> 0 <= y -> sqrt x <= sqrt y -> x <= y
Proof.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_alt :
  forall x y : R, x <= y -> sqrt x <= sqrt y.forall x y : R, x <= y -> sqrt x <= sqrt y
Proof.forall x y : R, x <= y -> sqrt x <= sqrt y
  intros x y [Hxy|Hxy].x, y:R
Hxy:x < y
sqrt x <= sqrt y
x, y:R
Hxy:x = y
sqrt x <= sqrt y
  destruct (Rle_or_lt 0 x) as [Hx|Hx].x, y:R
Hxy:x < y
Hx:0 <= x
sqrt x <= sqrt y
x, y:R
Hxy:x < y
Hx:x < 0
sqrt x <= sqrt y
x, y:R
Hxy:x = y
sqrt x <= sqrt y
  apply Rlt_le.x, y:R
Hxy:x < y
Hx:0 <= x
sqrt x < sqrt y
x, y:R
Hxy:x < y
Hx:x < 0
sqrt x <= sqrt y
x, y:R
Hxy:x = y
sqrt x <= sqrt y
  apply sqrt_lt_1_alt.x, y:R
Hxy:x < y
Hx:0 <= x
0 <= x < y
x, y:R
Hxy:x < y
Hx:x < 0
sqrt x <= sqrt y
x, y:R
Hxy:x = y
sqrt x <= sqrt y
  now split.x, y:R
Hxy:x < y
Hx:x < 0
sqrt x <= sqrt y
x, y:R
Hxy:x = y
sqrt x <= sqrt y
  unfold sqrt at 1.x, y:R
Hxy:x < y
Hx:x < 0
match Rcase_abs x with
| left _ => 0
| right a =>
    Rsqrt
      {| nonneg := x; cond_nonneg := Rge_le x 0 a |}
end <= sqrt y
x, y:R
Hxy:x = y
sqrt x <= sqrt y
  destruct (Rcase_abs x) as [Hx'|Hx'].x, y:R
Hxy:x < y
Hx, Hx':x < 0
0 <= sqrt y
x, y:R
Hxy:x < y
Hx:x < 0
Hx':x >= 0
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hx' |} <=
sqrt y
x, y:R
Hxy:x = y
sqrt x <= sqrt y
  apply sqrt_pos.x, y:R
Hxy:x < y
Hx:x < 0
Hx':x >= 0
Rsqrt {| nonneg := x; cond_nonneg := Rge_le x 0 Hx' |} <=
sqrt y
x, y:R
Hxy:x = y
sqrt x <= sqrt y
  now elim Rge_not_lt with (1 := Hx').x, y:R
Hxy:x = y
sqrt x <= sqrt y
  rewrite Hxy.x, y:R
Hxy:x = y
sqrt y <= sqrt y
  apply Rle_refl.
Qed.

Lemma sqrt_le_1 :
  forall x y:R, 0 <= x -> 0 <= y -> x <= y -> sqrt x <= sqrt y.forall x y : R,
0 <= x -> 0 <= y -> x <= y -> sqrt x <= sqrt y
Proof.forall x y : R,
0 <= x -> 0 <= y -> x <= y -> sqrt x <= sqrt y
  intros x y _ _ Hxy.x, y:R
Hxy:x <= y
sqrt x <= sqrt y
  now apply sqrt_le_1_alt.
Qed.

Lemma sqrt_inj : forall x y:R, 0 <= x -> 0 <= y -> sqrt x = sqrt y -> x = y.forall x y : R,
0 <= x -> 0 <= y -> sqrt x = sqrt y -> x = y
Proof.forall x y : R,
0 <= x -> 0 <= y -> sqrt x = sqrt y -> x = y
  intros; cut (Rsqr (sqrt x) = Rsqr (sqrt y)).x, y:R
H:0 <= x
H0:0 <= y
H1:sqrt x = sqrt y
(sqrt x)² = (sqrt y)² -> x = y
x, y:R
H:0 <= x
H0:0 <= y
H1:sqrt x = sqrt y
(sqrt x)² = (sqrt y)²
  intro; rewrite (Rsqr_sqrt x H) in H2; rewrite (Rsqr_sqrt y H0) in H2;
    assumption.x, y:R
H:0 <= x
H0:0 <= y
H1:sqrt x = sqrt y
(sqrt x)² = (sqrt y)²
  rewrite H1; reflexivity.
Qed.

Lemma sqrt_less_alt :
  forall x : R, 1 < x -> sqrt x < x.forall x : R, 1 < x -> sqrt x < x
Proof.forall x : R, 1 < x -> sqrt x < x
  intros x Hx.x:R
Hx:1 < x
sqrt x < x
  assert (Hx1 := Rle_lt_trans _ _ _ Rle_0_1 Hx).x:R
Hx:1 < x
Hx1:0 < x
sqrt x < x
  assert (Hx2 := Rlt_le _ _ Hx1).x:R
Hx:1 < x
Hx1:0 < x
Hx2:0 <= x
sqrt x < x
  apply Rsqr_incrst_0 ; trivial.x:R
Hx:1 < x
Hx1:0 < x
Hx2:0 <= x
(sqrt x)² < x²
x:R
Hx:1 < x
Hx1:0 < x
Hx2:0 <= x
0 <= sqrt x
  rewrite Rsqr_sqrt ; trivial.x:R
Hx:1 < x
Hx1:0 < x
Hx2:0 <= x
x < x²
x:R
Hx:1 < x
Hx1:0 < x
Hx2:0 <= x
0 <= sqrt x
  rewrite <- (Rmult_1_l x) at 1.x:R
Hx:1 < x
Hx1:0 < x
Hx2:0 <= x
1 * x < x²
x:R
Hx:1 < x
Hx1:0 < x
Hx2:0 <= x
0 <= sqrt x
  now apply Rmult_lt_compat_r.x:R
Hx:1 < x
Hx1:0 < x
Hx2:0 <= x
0 <= sqrt x
  apply sqrt_pos.
Qed.

Lemma sqrt_less : forall x:R, 0 <= x -> 1 < x -> sqrt x < x.forall x : R, 0 <= x -> 1 < x -> sqrt x < x
Proof.forall x : R, 0 <= x -> 1 < x -> sqrt x < x
  intros x _.x:R
1 < x -> sqrt x < x
  apply sqrt_less_alt.
Qed.

Lemma sqrt_more : forall x:R, 0 < x -> x < 1 -> x < sqrt x.forall x : R, 0 < x -> x < 1 -> x < sqrt x
Proof.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;
          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).forall a b c d : R,
a * c + b * d <= sqrt (a² + b²) * sqrt (c² + d²)
Proof.forall a b c d : R,
a * c + b * d <= sqrt (a² + b²) * sqrt (c² + d²)
  intros a b c d; apply Rsqr_incr_0_var;
    [ rewrite Rsqr_mult; 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 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; 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; 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 :
  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.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 * x² + b * x + c = 0
Proof.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 * x² + b * x + c = 0
  intros; elim H0; intro.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x1 a b c
a * x² + b * x + c = 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
a * x² + b * x + c = 0
  rewrite H1.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x1 a b c
a * (sol_x1 a b c)² + b * sol_x1 a b c + c = 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
a * x² + b * x + c = 0
  unfold sol_x1, Delta, Rsqr.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x1 a b c
a *
((- b + sqrt (b * b - 4 * a * c)) / (2 * a) *
 ((- b + sqrt (b * b - 4 * a * c)) / (2 * a))) +
b * ((- b + sqrt (b * b - 4 * a * c)) / (2 * a)) + c =
0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
a * x² + b * x + c = 0
  field_simplify.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x1 a b c
(4 * a * c - b ^ 2 + sqrt (b * b - 4 * a * c) ^ 2) /
(4 * a) = 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x1 a b c
a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
a * x² + b * x + c = 0
  rewrite <- (Rsqr_pow2 (sqrt _)), Rsqr_sqrt.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x1 a b c
(4 * a * c - b ^ 2 + (b * b - 4 * a * c)) / (4 * a) =
0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x1 a b c
0 <= b * b - 4 * a * c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x1 a b c
a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
a * x² + b * x + c = 0
  field.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x1 a b c
a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x1 a b c
0 <= b * b - 4 * a * c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x1 a b c
a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
a * x² + b * x + c = 0
  apply a.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x1 a b c
0 <= b * b - 4 * a * c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x1 a b c
a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
a * x² + b * x + c = 0
  apply H.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x1 a b c
a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
a * x² + b * x + c = 0
  apply a.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
a * x² + b * x + c = 0
  rewrite H1.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
a * (sol_x2 a b c)² + b * sol_x2 a b c + c = 0
  unfold sol_x2, Delta, Rsqr.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
a *
((- b - sqrt (b * b - 4 * a * c)) / (2 * a) *
 ((- b - sqrt (b * b - 4 * a * c)) / (2 * a))) +
b * ((- b - sqrt (b * b - 4 * a * c)) / (2 * a)) + c =
0
  field_simplify.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
(4 * a * c - b ^ 2 + sqrt (b * b - 4 * a * c) ^ 2) /
(4 * a) = 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
a <> 0
  rewrite <- (Rsqr_pow2 (sqrt _)), Rsqr_sqrt.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
(4 * a * c - b ^ 2 + (b * b - 4 * a * c)) / (4 * a) =
0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
0 <= b * b - 4 * a * c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
a <> 0
  field.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
0 <= b * b - 4 * a * c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
a <> 0
  apply a.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
0 <= b * b - 4 * a * c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
a <> 0
  apply H.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:x = sol_x1 a b c \/ x = sol_x2 a b c
H1:x = sol_x2 a b c
a <> 0
  apply a.
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.forall (a : nonzeroreal) (b c x : R),
Delta_is_pos a b c ->
a * x² + b * x + c = 0 ->
x = sol_x1 a b c \/ x = sol_x2 a b c
Proof.forall (a : nonzeroreal) (b c x : R),
Delta_is_pos a b c ->
a * 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).a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c ->
a * (x + b / (2 * a))² =
- ((4 * a * c - b²) / (4 * a)) ->
x = sol_x1 a b c \/ x = sol_x2 a b c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
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)).a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
a * (x + b / (2 * a))² = (b² - 4 * a * c) / (4 * a) ->
x = sol_x1 a b c \/ x = sol_x2 a b c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  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))).a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (Delta a b c / (4 * a)) ->
x = sol_x1 a b c \/ x = sol_x2 a b c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  replace (/ a * (Delta a b c / (4 * a))) with
  (Rsqr (sqrt (Delta a b c) / (2 * a))).a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = (sqrt (Delta a b c) / (2 * a))² ->
x = sol_x1 a b c \/ x = sol_x2 a b c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(sqrt (Delta a b c) / (2 * a))² =
/ a * (Delta a b c / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  intro;
    generalize (Rsqr_eq (x + b / (2 * a)) (sqrt (Delta a b c) / (2 * a)) H3);
      intro; elim H4; intro.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
H3:(x + b / (2 * a))² =
(sqrt (Delta a b c) / (2 * a))²
H4:x + b / (2 * a) = sqrt (Delta a b c) / (2 * a) \/
x + b / (2 * a) =
- (sqrt (Delta a b c) / (2 * a))
H5:x + b / (2 * a) = sqrt (Delta a b c) / (2 * a)
x = sol_x1 a b c \/ x = sol_x2 a b c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
H3:(x + b / (2 * a))² =
(sqrt (Delta a b c) / (2 * a))²
H4:x + b / (2 * a) = sqrt (Delta a b c) / (2 * a) \/
x + b / (2 * a) =
- (sqrt (Delta a b c) / (2 * a))
H5:x + b / (2 * a) =
- (sqrt (Delta a b c) / (2 * a))
x = sol_x1 a b c \/ x = sol_x2 a b c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(sqrt (Delta a b c) / (2 * a))² =
/ a * (Delta a b c / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  left; unfold sol_x1;
    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.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
H3:(x + b / (2 * a))² =
(sqrt (Delta a b c) / (2 * a))²
H4:x + b / (2 * a) = sqrt (Delta a b c) / (2 * a) \/
x + b / (2 * a) =
- (sqrt (Delta a b c) / (2 * a))
H5:x + b / (2 * a) = sqrt (Delta a b c) / (2 * a)
x = - (b / (2 * a)) + sqrt (Delta a b c) / (2 * a) ->
x = (- b + sqrt (Delta a b c)) / (2 * a)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
H3:(x + b / (2 * a))² =
(sqrt (Delta a b c) / (2 * a))²
H4:x + b / (2 * a) = sqrt (Delta a b c) / (2 * a) \/
x + b / (2 * a) =
- (sqrt (Delta a b c) / (2 * a))
H5:x + b / (2 * a) = sqrt (Delta a b c) / (2 * a)
x = - (b / (2 * a)) + (x + b / (2 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
H3:(x + b / (2 * a))² =
(sqrt (Delta a b c) / (2 * a))²
H4:x + b / (2 * a) = sqrt (Delta a b c) / (2 * a) \/
x + b / (2 * a) =
- (sqrt (Delta a b c) / (2 * a))
H5:x + b / (2 * a) =
- (sqrt (Delta a b c) / (2 * a))
x = sol_x1 a b c \/ x = sol_x2 a b c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(sqrt (Delta a b c) / (2 * a))² =
/ a * (Delta a b c / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  intro; rewrite H6; unfold Rdiv; ring.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
H3:(x + b / (2 * a))² =
(sqrt (Delta a b c) / (2 * a))²
H4:x + b / (2 * a) = sqrt (Delta a b c) / (2 * a) \/
x + b / (2 * a) =
- (sqrt (Delta a b c) / (2 * a))
H5:x + b / (2 * a) = sqrt (Delta a b c) / (2 * a)
x = - (b / (2 * a)) + (x + b / (2 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
H3:(x + b / (2 * a))² =
(sqrt (Delta a b c) / (2 * a))²
H4:x + b / (2 * a) = sqrt (Delta a b c) / (2 * a) \/
x + b / (2 * a) =
- (sqrt (Delta a b c) / (2 * a))
H5:x + b / (2 * a) =
- (sqrt (Delta a b c) / (2 * a))
x = sol_x1 a b c \/ x = sol_x2 a b c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(sqrt (Delta a b c) / (2 * a))² =
/ a * (Delta a b c / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  ring.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
H3:(x + b / (2 * a))² =
(sqrt (Delta a b c) / (2 * a))²
H4:x + b / (2 * a) = sqrt (Delta a b c) / (2 * a) \/
x + b / (2 * a) =
- (sqrt (Delta a b c) / (2 * a))
H5:x + b / (2 * a) =
- (sqrt (Delta a b c) / (2 * a))
x = sol_x1 a b c \/ x = sol_x2 a b c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(sqrt (Delta a b c) / (2 * a))² =
/ a * (Delta a b c / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  right; unfold sol_x2;
    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.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
H3:(x + b / (2 * a))² =
(sqrt (Delta a b c) / (2 * a))²
H4:x + b / (2 * a) = sqrt (Delta a b c) / (2 * a) \/
x + b / (2 * a) =
- (sqrt (Delta a b c) / (2 * a))
H5:x + b / (2 * a) =
- (sqrt (Delta a b c) / (2 * a))
x = - (b / (2 * a)) + - (sqrt (Delta a b c) / (2 * a)) ->
x = (- b - sqrt (Delta a b c)) / (2 * a)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
H3:(x + b / (2 * a))² =
(sqrt (Delta a b c) / (2 * a))²
H4:x + b / (2 * a) = sqrt (Delta a b c) / (2 * a) \/
x + b / (2 * a) =
- (sqrt (Delta a b c) / (2 * a))
H5:x + b / (2 * a) =
- (sqrt (Delta a b c) / (2 * a))
x = - (b / (2 * a)) + (x + b / (2 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(sqrt (Delta a b c) / (2 * a))² =
/ a * (Delta a b c / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  intro; rewrite H6; unfold Rdiv; ring.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
H3:(x + b / (2 * a))² =
(sqrt (Delta a b c) / (2 * a))²
H4:x + b / (2 * a) = sqrt (Delta a b c) / (2 * a) \/
x + b / (2 * a) =
- (sqrt (Delta a b c) / (2 * a))
H5:x + b / (2 * a) =
- (sqrt (Delta a b c) / (2 * a))
x = - (b / (2 * a)) + (x + b / (2 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(sqrt (Delta a b c) / (2 * a))² =
/ a * (Delta a b c / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  ring.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(sqrt (Delta a b c) / (2 * a))² =
/ a * (Delta a b c / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  rewrite Rsqr_div.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(sqrt (Delta a b c))² / (2 * a)² =
/ a * (Delta a b c / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
2 * a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  rewrite Rsqr_sqrt.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
Delta a b c / (2 * a)² = / a * (Delta a b c / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
0 <= Delta a b c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
2 * a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  unfold Rdiv.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
Delta a b c * / (2 * a)² =
/ a * (Delta a b c * / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
0 <= Delta a b c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
2 * a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  repeat rewrite Rmult_assoc.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
Delta a b c * / (2 * a)² =
/ a * (Delta a b c * / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
0 <= Delta a b c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
2 * a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  rewrite (Rmult_comm (/ a)).a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
Delta a b c * / (2 * a)² =
Delta a b c * / (4 * a) * / a
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
0 <= Delta a b c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
2 * a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  rewrite Rmult_assoc.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
Delta a b c * / (2 * a)² =
Delta a b c * (/ (4 * a) * / a)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
0 <= Delta a b c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
2 * a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  rewrite <- Rinv_mult_distr.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
Delta a b c * / (2 * a)² = Delta a b c * / (4 * a * a)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
4 * a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
0 <= Delta a b c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
2 * a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  replace (4 * a * a) with (Rsqr (2 * a)).a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
Delta a b c * / (2 * a)² = Delta a b c * / (2 * a)²
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(2 * a)² = 4 * a * a
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
4 * a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
0 <= Delta a b c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
2 * a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  reflexivity.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(2 * a)² = 4 * a * a
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
4 * a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
0 <= Delta a b c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
2 * a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  ring_Rsqr.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
4 * a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
0 <= Delta a b c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
2 * a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  apply prod_neq_R0;
    [ discrR | apply (cond_nonzero a) ].a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
0 <= Delta a b c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
2 * a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  apply (cond_nonzero a).a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
0 <= Delta a b c
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
2 * a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  assumption.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
2 * a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  apply prod_neq_R0; [ discrR | apply (cond_nonzero a) ].a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = / a * (a * (x + b / (2 * a))²)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
(x + b / (2 * a))² = 1 * (x + b / (2 * a))²
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  symmetry ; apply Rmult_1_l.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
H2:a * (x + b / (2 * a))² = Delta a b c / (4 * a)
a <> 0
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  apply (cond_nonzero a).a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) / (4 * a) =
- ((4 * a * c - b²) / (4 * a))
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  unfold Rdiv; rewrite <- Ropp_mult_distr_l_reverse.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) * / (4 * a) =
- (4 * a * c - b²) * / (4 * a)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  rewrite Ropp_minus_distr.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
H1:b² - 4 * a * c = Delta a b c
(b² - 4 * a * c) * / (4 * a) =
(b² - 4 * a * c) * / (4 * a)
a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  reflexivity.a:nonzeroreal
b, c, x:R
H:Delta_is_pos a b c
H0:(4 * a * c - b²) / (4 * a) +
a * (x + b / (2 * a))² = 0
b² - 4 * a * c = Delta a b c
  reflexivity.
Qed.