proposition: Theorem RND_Max_Pos_canonic : forall r : R, (0 <= r)%R -> Fcanonic radix b (RND_Max_Pos r).
proof: Proof. intros r H; unfold RND_Max_Pos in |- *. case (Req_EM_T r (RND_Min_Pos r)); intros H1. apply RND_Min_Pos_canonic; auto. apply FSuccCanonic; auto with zarith; apply RND_Min_Pos_canonic; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz