fact: Definition sin prec xi := match xi with | Ibnd xl xu => if F'.le' xu xl then T.sin_fast prec xl else let pi4 := T.pi4 prec in let pi2 := F.mul_DN prec (lower pi4) c2 in match F'.le' (F.neg pi2) xl, F'.le' xu pi2 with | true, true => bnd (lower (T.sin_fast prec xl)) (upper (T.sin_fast prec xu)) | true, false => cos prec (sub prec (mul2 prec pi4) xi) | _, _ => neg (cos prec (add prec xi (mul2 prec pi4))) end | Inan => Inan end.
imports: Coq(Reals Psatz) Xreal Basic Sig Interval Float Transcend