proposition: Lemma Xpower_int_correct : forall n, extension (fun x => powerRZ x n) (fun x => Xpower_int x n).
proof: Proof. intros [|n|n] [|x] ; try split. unfold Xpower_int, Xpower_int', Xbind. now case (is_zero x). Qed.
imports: Coq(Reals Bool) Flocq(Raux) mathcomp.ssreflect(ssreflect) Stdlib