proposition: Lemma power_int_propagate : forall prec n, propagate (fun x => I.power_int prec x n).
proof: Proof. intros prec n. apply propagate_extension with (1 := I.power_int_correct prec n). Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic