Library Coq.Reals.R_sqrt
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_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 :
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 :
forall x y:R, 0 <=
x -> 0 <
y ->
sqrt (
x /
y) =
sqrt x /
sqrt y.
Lemma sqrt_lt_0 :
forall x y:R, 0 <=
x -> 0 <=
y ->
sqrt x <
sqrt y ->
x <
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 :
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 :
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).
Resolution of a*X^2+b*X+c=0