proposition: Lemma Rsqr_eq_asb_1 : forall x y:R, Rabs x = Rabs y -> Rsqr x = Rsqr y.
proof: Proof. intros; cut (Rsqr (Rabs x) = Rsqr (Rabs y)). - intro; repeat rewrite <- Rsqr_abs in H0; assumption. - rewrite H; reflexivity. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun