fact: Definition cos_fast prec x := match F'.cmp x F.zero with | Xeq => i1 | Xlt => cos_fastP prec (F.neg x) | Xgt => cos_fastP prec x | Xund => I.nai end.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float