proposition: Lemma neg_pos_Rsqr_lt : forall x y : R, - y < x -> x < y -> Rsqr x < Rsqr y.
proof: Proof. intros x y Hneg Hpos. destruct (Rcase_abs x) as [Hlt|HLe]. - rewrite (Rsqr_neg x); apply Rsqr_incrst_1. + rewrite <- (Ropp_involutive y); apply Ropp_lt_contravar; exact Hneg. + rewrite <- (Ropp_0). apply Ropp_le_contravar, Rlt_le; exact Hlt. + apply (Rlt_trans _ _ _ Hneg) in Hlt. rewrite <- (Ropp_0) in Hlt; apply Ropp_lt_cancel in Hlt; apply Rlt_le; exact Hlt. - apply Rsqr_incrst_1. + exact Hpos. + apply Rge_le; exact HLe. + apply Rge_le in HLe. apply (Rle_lt_trans _ _ _ HLe), Rlt_le in Hpos; exact Hpos. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun