fact: Definition RND_EvenClosest (r : R) := match Rle_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r)) with | left H => match Rle_lt_or_eq_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r)) H with | left _ => RND_Max r | right _ => match OddEvenDec (Fnum (RND_Min r)) with | left _ => RND_Max r | right _ => RND_Min r end end | right _ => RND_Min r end.
imports: Reals ZArith List PeanoNat Psatz