proposition: Lemma neg_pos_Rsqr_le : forall x y:R, - y <= x -> x <= y -> Rsqr x <= Rsqr y.
proof: Proof. intros x y H H0; destruct (Rcase_abs x) as [Hlt|Hle]. - apply Ropp_lt_gt_contravar, Rlt_le in Hlt; rewrite Ropp_0 in Hlt; apply Ropp_le_ge_contravar, Rge_le in H; rewrite Ropp_involutive in H. assert (0 <= y) by (apply Rle_trans with (-x); assumption). rewrite (Rsqr_neg x); apply Rsqr_incr_1; assumption. - apply Rge_le in Hle; assert (0 <= y) by (apply Rle_trans with x; assumption). apply Rsqr_incr_1; assumption. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun