fact: Definition RND_Closest (r : R) := let ru := RND_Max b beta p r in let rd := RND_Min b beta p r in match Rle_dec (Rabs (ru - r)) (Rabs (rd - r)) with | left H => match Rle_lt_or_eq_dec (Rabs (ru - r)) (Rabs (rd - r)) H with | left _ => ru | right _ => match choice (Zfloor (scaled_mantissa beta (FLT_exp (- dExp b) p) r)) with | true => ru | false => rd end end | right _ => rd end.
imports: Coq(Lia) Pff Core