fact: Definition power_int prec xi n := match n with | Zpos p => power_pos prec xi p | Z0 => match xi with Inan => Inan | _ => Ibnd c1 c1 end | Zneg p => inv prec (power_pos prec xi p) end.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval