proposition: Lemma Rsqr_neg_pos_le_1 : forall x y:R, - y <= x -> x <= y -> 0 <= y -> Rsqr x <= Rsqr y.
proof: Proof. intros x y H H0 H1; 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; rewrite (Rsqr_neg x); apply Rsqr_incr_1; assumption. - apply Rge_le in Hle; apply Rsqr_incr_1; assumption. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun