proposition: Theorem RND_Max_Pos_Rle : forall r : R, (0 <= r)%R -> (r <= RND_Max_Pos r)%R.
proof: Proof. intros r H. unfold RND_Max_Pos in |- *; case (Req_EM_T r (RND_Min_Pos r)); intros H1. rewrite <- H1; auto with real. case (Rle_or_lt r (FSucc b radix p (RND_Min_Pos r))); auto; intros H2. generalize (RND_Min_Pos_correct r H); intros T; elim T; intros H3 T1; elim T1; intros H4 H5; clear T T1. absurd (FSucc b radix p (RND_Min_Pos r) <= RND_Min_Pos r)%R; auto with zarith real. apply Rlt_not_le; auto with zarith. unfold FtoRradix in |- *; apply FSuccLt; auto with zarith. apply H5; auto with real. apply FBoundedSuc; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz