fact: Fixpoint Fpower_pos_UP prec x n := match n with | xH => x | xO p => Fpower_pos_UP prec (F.mul_UP prec x x) p | xI p => F.mul_UP prec x (Fpower_pos_UP prec (F.mul_UP prec x x) p) end.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval