proposition: Theorem RND_Closest_canonic : forall r : R, Fcanonic beta b (RND_Closest r).
proof: Proof. intros r; unfold RND_Closest in |- *. case (Rle_dec _ _ ); intros H1. case (Rle_lt_or_eq_dec _ _ H1); intros H2. apply RND_Max_canonic; try easy; apply radix_gt_1. case (choice _). now apply RND_Max_canonic; try easy; apply radix_gt_1. now apply RND_Min_canonic; try easy; apply radix_gt_1. now apply RND_Min_canonic; try easy; apply radix_gt_1. Qed.
imports: Coq(Lia) Pff Core