proposition: Lemma Rsqr_neg_pos_le_0 : forall x y:R, Rsqr x <= Rsqr y -> 0 <= y -> - y <= x.
proof: Proof. intros; destruct (Rcase_abs x) as [Hlt|Hle]. - generalize (Ropp_lt_gt_contravar x 0 Hlt); rewrite Ropp_0; intro; generalize (Rlt_le 0 (- x) H1); intro; rewrite (Rsqr_neg x) in H; generalize (Rsqr_incr_0 (- x) y H H2 H0); intro; rewrite <- (Ropp_involutive x); apply Ropp_ge_le_contravar; apply Rle_ge; assumption. - apply Rle_trans with 0; [ rewrite <- Ropp_0; apply Ropp_ge_le_contravar; apply Rle_ge; assumption | apply Rge_le; assumption ]. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun