Library Coq.Reals.R_sqr

Require Import Rdefinitions Raxioms RIneq.
Require Import Rbasic_fun.
Local Open Scope R_scope.

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' x y : Rsqr (x / y) = Rsqr x / Rsqr y.

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

#[deprecated(since="8.16",note="Use Rsqr_div'.")]
Notation Rsqr_div := Rsqr_div_depr.

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' x : Rsqr (/ x) = / Rsqr x.

Lemma Rsqr_inv_depr : forall x:R, x <> 0 -> Rsqr (/ x) = / Rsqr x.

#[deprecated(since="8.16",note="Use Rsqr_inv'.")]
Notation Rsqr_inv := Rsqr_inv_depr.

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.