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 neg_pos_Rsqr_lt :
forall x y :
R,
- y < x -> x < y -> Rsqr x < Rsqr y.
Lemma Rsqr_bounds_le :
forall a b:
R,
-a <= b <= a -> 0
<= Rsqr b <= Rsqr a.
Lemma Rsqr_bounds_lt :
forall a b:
R,
-a < b < a -> 0
<= Rsqr b < Rsqr a.
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.