proposition: Lemma power_int_correct : forall prec n, extension (fun x => powerRZ x n) (fun xi => I.power_int prec xi n).
proof: Proof. intros prec n xi x Hx. generalize (I.power_int_correct prec n xi _ Hx). unfold Xpower_int, Xpower_int', Xbind. destruct n as [|n|n] ; try easy. case is_zero ; try easy. now case I.convert. Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic