Library Coq.Reals.R_sqr
Rsqr : some results
Ltac ring_Rsqr :=
unfold Rsqr in |- *;
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.