proposition: Lemma Rsqr_pow2 : forall x, Rsqr x = x ^ 2.
proof: Proof. intros; unfold Rsqr; simpl; rewrite Rmult_1_r; reflexivity. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac