proposition: Theorem power_int_correct : forall prec n, extension (fun x => Xpower_int x n) (fun x => power_int prec x n).
proof: Proof. intros prec [|n|n]. { unfold power_int, Xpower_int. intros [ | xl xu] [ | x] ; try ( intros ; exact I ) ; [now unfold convert; case (_ && _)|]. intros _. simpl. unfold c1. rewrite F.fromZ_correct by easy. rewrite F'.valid_lb_real, ?F'.valid_ub_real; [|now rewrite F.real_correct, F.fromZ_correct..]. split ; apply Rle_refl. } { apply power_pos_correct. } intros xi x Hx. generalize (power_pos_correct prec n _ _ Hx). intros Hp. generalize (inv_correct prec _ _ Hp). unfold Xpower_int, Xpower_int', Xinv', Xbind, power_int. destruct x as [ | x]; [easy|]. replace (is_zero x) with (is_zero (x ^ nat_of_P n)); [easy|]. case (is_zero_spec x) ; intros Zx. { rewrite Zx, pow_i. { apply is_zero_0. } apply lt_O_nat_of_P. } case is_zero_spec ; try easy. intros H. elim (pow_nonzero _ _ Zx H). Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval