proposition: Theorem RND_EvenClosest_canonic : forall r : R, Fcanonic radix b (RND_EvenClosest r).
proof: Proof. intros r; unfold RND_EvenClosest in |- *. case (Rle_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r))); intros H1. case (Rle_lt_or_eq_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r)) H1); intros H2. apply RND_Max_canonic. case (OddEvenDec (Fnum (RND_Min r))); intros H3. apply RND_Max_canonic. apply RND_Min_canonic. apply RND_Min_canonic. Qed.
imports: Reals ZArith List PeanoNat Psatz