proposition: Lemma Rsqr_eq_abs_0 : forall x y:R, Rsqr x = Rsqr y -> Rabs x = Rabs y.
proof: Proof. intros; unfold Rabs; case (Rcase_abs x) as [Hltx|Hgex]; case (Rcase_abs y) as [Hlty|Hgey]. - rewrite (Rsqr_neg x), (Rsqr_neg y) in H; generalize (Ropp_lt_gt_contravar y 0 Hlty); generalize (Ropp_lt_gt_contravar x 0 Hltx); rewrite Ropp_0; intros; generalize (Rlt_le 0 (- x) H0); generalize (Rlt_le 0 (- y) H1); intros; apply Rsqr_inj; assumption. - rewrite (Rsqr_neg x) in H; generalize (Rge_le y 0 Hgey); intro; generalize (Ropp_lt_gt_contravar x 0 Hltx); rewrite Ropp_0; intro; generalize (Rlt_le 0 (- x) H1); intro; apply Rsqr_inj; assumption. - rewrite (Rsqr_neg y) in H; generalize (Rge_le x 0 Hgex); intro; generalize (Ropp_lt_gt_contravar y 0 Hlty); rewrite Ropp_0; intro; generalize (Rlt_le 0 (- y) H1); intro; apply Rsqr_inj; assumption. - apply Rsqr_inj; auto using Rge_le. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun