fact: Fixpoint Fpower_pos_DN prec x n := match n with | xH => x | xO p => let xx := F.mul_DN prec x x in match F.cmp xx F.zero with | Xgt => Fpower_pos_DN prec xx p | Xeq | Xlt => F.zero | Xund => F.nan end | xI p => let xx := F.mul_DN prec x x in match F.cmp xx F.zero with | Xgt => F.mul_DN prec x (Fpower_pos_DN prec xx p) | Xeq | Xlt => F.zero | Xund => F.nan end end.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval