fact: Definition cos prec xi := match abs xi with | Ibnd xl xu => if F'.le' xu xl then T.cos_fast prec xl else let pi4 := T.pi4 prec in if F'.le' xu (F.mul_DN prec (lower pi4) c4) then bnd (lower (T.cos_fast prec xu)) (upper (T.cos_fast prec xl)) else if F'.le' xu (F.mul_DN prec (lower pi4) c8) then if F'.le' (F.mul_UP prec (upper pi4) c4) xl then bnd (lower (T.cos_fast prec xl)) (upper (T.cos_fast prec xu)) else bnd cm1 (F.max (upper (T.cos_fast prec xl)) (upper (T.cos_fast prec xu))) else let d := F.sub_UP prec xu xl in if F'.le' d c3 then let m := F.midpoint xl xu in let d := F.max (F.sub_UP prec xu m) (F.sub_UP prec m xl) in let c := T.cos_fast prec m in meet (bnd cm1 c1) (add prec c (bnd (F.neg d) d)) else bnd cm1 c1 | Inan => Inan end.
imports: Coq(Reals Psatz) Xreal Basic Sig Interval Float Transcend