fact: Definition cos_fastP prec x := let th := c1_2 in match F'.le' x th with | true => cos_fast0 prec x | _ => let m := F.StoZ (F.mag x) in let prec := F.incr_prec prec (Z2P (m + 6)) in snd (sin_cos_reduce prec x (S (Z2nat m))) end.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float