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.