fact: Definition error_aux prec mode e := let e := match mode with | rnd_NE => Z.pred e | _ => e end in let err := F.pow2_UP prec (F.ZtoS e) in match mode with | rnd_NE => Ibnd (F.neg err) err | rnd_UP => Ibnd F.zero err | rnd_DN => Ibnd (F.neg err) F.zero | rnd_ZR => Ibnd (F.neg err) err end.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval