Library Coq.Reals.R_sqr
Rsqr : some results
Ltac ring_Rsqr :=
unfold Rsqr;
ring.
Lemma Rsqr_neg :
forall x:
R,
Rsqr x = Rsqr (
- x).
Lemma Rsqr_mult :
forall x y:
R,
Rsqr (
x * y)
= Rsqr x * Rsqr y.
Lemma Rsqr_plus :
forall x y:
R,
Rsqr (
x + y)
= Rsqr x + Rsqr y + 2
* x * y.
Lemma Rsqr_minus :
forall x y:
R,
Rsqr (
x - y)
= Rsqr x + Rsqr y - 2
* x * y.
Lemma Rsqr_neg_minus :
forall x y:
R,
Rsqr (
x - y)
= Rsqr (
y - x).
Lemma Rsqr_1 :
Rsqr 1
= 1.
Lemma Rsqr_gt_0_0 :
forall x:
R, 0
< Rsqr x ->
x <> 0.
Lemma Rsqr_pos_lt :
forall x:
R,
x <> 0 -> 0
< Rsqr x.
Lemma Rsqr_div :
forall x y:
R,
y <> 0 ->
Rsqr (
x / y)
= Rsqr x / Rsqr y.
Lemma Rsqr_eq_0 :
forall x:
R,
Rsqr x = 0 ->
x = 0.
Lemma Rsqr_minus_plus :
forall a b:
R,
(a - b) * (a + b) = Rsqr a - Rsqr b.
Lemma Rsqr_plus_minus :
forall a b:
R,
(a + b) * (a - b) = Rsqr a - Rsqr b.
Lemma Rsqr_incr_0 :
forall x y:
R,
Rsqr x <= Rsqr y -> 0
<= x -> 0
<= y ->
x <= y.
Lemma Rsqr_incr_0_var :
forall x y:
R,
Rsqr x <= Rsqr y -> 0
<= y ->
x <= y.
Lemma Rsqr_incr_1 :
forall x y:
R,
x <= y -> 0
<= x -> 0
<= y ->
Rsqr x <= Rsqr y.
Lemma Rsqr_incrst_0 :
forall x y:
R,
Rsqr x < Rsqr y -> 0
<= x -> 0
<= y ->
x < y.
Lemma Rsqr_incrst_1 :
forall x y:
R,
x < y -> 0
<= x -> 0
<= y ->
Rsqr x < Rsqr y.
Lemma Rsqr_neg_pos_le_0 :
forall x y:
R,
Rsqr x <= Rsqr y -> 0
<= y ->
- y <= x.
Lemma Rsqr_neg_pos_le_1 :
forall x y:
R,
- y <= x ->
x <= y -> 0
<= y ->
Rsqr x <= Rsqr y.
Lemma neg_pos_Rsqr_le :
forall x y:
R,
- y <= x ->
x <= y ->
Rsqr x <= Rsqr y.
Lemma Rsqr_abs :
forall x:
R,
Rsqr x = Rsqr (
Rabs x).
Lemma Rsqr_le_abs_0 :
forall x y:
R,
Rsqr x <= Rsqr y ->
Rabs x <= Rabs y.
Lemma Rsqr_le_abs_1 :
forall x y:
R,
Rabs x <= Rabs y ->
Rsqr x <= Rsqr y.
Lemma Rsqr_lt_abs_0 :
forall x y:
R,
Rsqr x < Rsqr y ->
Rabs x < Rabs y.
Lemma Rsqr_lt_abs_1 :
forall x y:
R,
Rabs x < Rabs y ->
Rsqr x < Rsqr y.
Lemma Rsqr_inj :
forall x y:
R, 0
<= x -> 0
<= y ->
Rsqr x = Rsqr y ->
x = y.
Lemma Rsqr_eq_abs_0 :
forall x y:
R,
Rsqr x = Rsqr y ->
Rabs x = Rabs y.
Lemma Rsqr_eq_asb_1 :
forall x y:
R,
Rabs x = Rabs y ->
Rsqr x = Rsqr y.
Lemma triangle_rectangle :
forall x y z:
R,
0
<= z ->
Rsqr x + Rsqr y <= Rsqr z ->
- z <= x <= z /\ - z <= y <= z.
Lemma triangle_rectangle_lt :
forall x y z:
R,
Rsqr x + Rsqr y < Rsqr z ->
Rabs x < Rabs z /\ Rabs y < Rabs z.
Lemma triangle_rectangle_le :
forall x y z:
R,
Rsqr x + Rsqr y <= Rsqr z ->
Rabs x <= Rabs z /\ Rabs y <= Rabs z.
Lemma Rsqr_inv :
forall x:
R,
x <> 0 ->
Rsqr (
/ x)
= / Rsqr x.
Lemma canonical_Rsqr :
forall (
a:
nonzeroreal) (
b c x:
R),
a * Rsqr x + b * x + c =
a * Rsqr (
x + b / (2
* a))
+ (4
* a * c - Rsqr b) / (4
* a).
Lemma Rsqr_eq :
forall x y:
R,
Rsqr x = Rsqr y ->
x = y \/ x = - y.