fact: Definition power_pos prec xi n := match xi with | Ibnd xl xu => match sign_large_ xl xu with | Xund => match n with | xH => xi | xO _ => let xm := F.max (F.abs xl) xu in Ibnd F.zero (Fpower_pos_UP prec xm n) | xI _ => Ibnd (F.neg (Fpower_pos_UP prec (F.abs xl) n)) (Fpower_pos_UP prec xu n) end | Xeq => Ibnd F.zero F.zero | Xlt => match n with | xH => xi | xO _ => Ibnd (Fpower_pos_DN prec (F.abs xu) n) (Fpower_pos_UP prec (F.abs xl) n) | xI _ => Ibnd (F.neg (Fpower_pos_UP prec (F.abs xl) n)) (F.neg (Fpower_pos_DN prec (F.abs xu) n)) end | Xgt => Ibnd (Fpower_pos_DN prec xl n) (Fpower_pos_UP prec xu n) end | _ => Inan end.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval