fact: Definition no_floor_op op := match op with | Nearbyint _ => false | RoundFlt _ _ _ | ErrorFlt _ _ _ => false | RoundFix _ _ | ErrorFix _ _ => false | _ => true end.
imports: Coq(Bool Reals) Flocq(Zaux Raux) Coq(List) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect) Stdlib Coquelicot Xreal Xreal_derive Basic Interval Interval_compl Taylor_model Tree Prog