proposition: Lemma sqrt_correct : forall prec, extension sqrt (I.sqrt prec).
proof: Proof. intros prec xi x Hx. generalize (I.sqrt_correct prec xi _ Hx). unfold Xsqrt', Xbind. case is_negative ; try easy. Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic