proposition: Lemma Rsqr_eq : forall x y:R, Rsqr x = Rsqr y -> x = y \/ x = - y.
proof: Proof. intros; unfold Rsqr in H; generalize (Rplus_eq_compat_l (- (y * y)) (x * x) (y * y) H); rewrite Rplus_opp_l; replace (- (y * y) + x * x) with ((x - y) * (x + y)). - intro; generalize (Rmult_integral (x - y) (x + y) H0); intro; elim H1; intros. + left; apply Rminus_diag_uniq; assumption. + right; apply Rminus_diag_uniq; unfold Rminus; rewrite Ropp_involutive; assumption. - ring. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun