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

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.

Lemma sqrt_positivity : forall x:R, 0 <= x -> 0 <= sqrt x.

Lemma sqrt_sqrt : forall x:R, 0 <= x -> sqrt x * sqrt x = x.

Lemma sqrt_0 : sqrt 0 = 0.

Lemma sqrt_1 : sqrt 1 = 1.

Lemma sqrt_eq_0 : forall x:R, 0 <= x -> sqrt x = 0 -> x = 0.

Lemma sqrt_lem_0 : forall x y:R, 0 <= x -> 0 <= y -> sqrt x = y -> y * y = x.

Lemma sqrt_lem_1 : forall x y:R, 0 <= x -> 0 <= y -> y * y = x -> sqrt x = y.

Lemma sqrt_def : forall x:R, 0 <= x -> sqrt x * sqrt x = x.

Lemma sqrt_square : forall x:R, 0 <= x -> sqrt (x * x) = x.

Lemma sqrt_Rsqr : forall x:R, 0 <= x -> sqrt (Rsqr x) = x.

Lemma sqrt_Rsqr_abs : forall x:R, sqrt (Rsqr x) = Rabs x.

Lemma Rsqr_sqrt : forall x:R, 0 <= x -> Rsqr (sqrt x) = x.

Lemma sqrt_mult_alt :
  forall x y : R, 0 <= x -> sqrt (x * y) = sqrt x * sqrt y.

Lemma sqrt_mult :
  forall x y:R, 0 <= x -> 0 <= y -> sqrt (x * y) = sqrt x * sqrt y.

Lemma sqrt_lt_R0 : forall x:R, 0 < x -> 0 < sqrt x.

Lemma sqrt_div_alt :
  forall x y : R, 0 < y -> sqrt (x / y) = sqrt x / sqrt y.

Lemma sqrt_div :
  forall x y:R, 0 <= x -> 0 < y -> sqrt (x / y) = sqrt x / sqrt y.

Lemma sqrt_lt_0_alt :
  forall x y : R, sqrt x < sqrt y -> x < y.

Lemma sqrt_lt_0 : forall x y:R, 0 <= x -> 0 <= y -> sqrt x < sqrt y -> x < y.

Lemma sqrt_lt_1_alt :
  forall x y : R, 0 <= x < y -> sqrt x < sqrt y.

Lemma sqrt_lt_1 : forall x y:R, 0 <= x -> 0 <= y -> x < y -> sqrt x < sqrt y.

Lemma sqrt_le_0 :
  forall x y:R, 0 <= x -> 0 <= y -> sqrt x <= sqrt y -> x <= y.

Lemma sqrt_le_1_alt :
  forall x y : R, x <= y -> sqrt x <= sqrt y.

Lemma sqrt_le_1 :
  forall x y:R, 0 <= x -> 0 <= y -> x <= y -> sqrt x <= sqrt y.

Lemma sqrt_inj : forall x y:R, 0 <= x -> 0 <= y -> sqrt x = sqrt y -> x = y.

Lemma sqrt_less_alt :
  forall x : R, 1 < x -> sqrt x < x.

Lemma sqrt_less : forall x:R, 0 <= x -> 1 < x -> sqrt x < x.

Lemma sqrt_more : forall x:R, 0 < x -> x < 1 -> x < sqrt x.

Lemma sqrt_cauchy :
  forall a b c d:R,
    a * c + b * d <= sqrt (Rsqr a + Rsqr b) * sqrt (Rsqr c + Rsqr d).

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.

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.