proposition: Theorem RND_Max_Pos_correct : forall r : R, (0 <= r)%R -> isMax b radix r (RND_Max_Pos r).
proof: Proof. intros r H. split. apply FcanonicBound with radix; apply RND_Max_Pos_canonic; auto. split. apply RND_Max_Pos_Rle; auto. unfold RND_Max_Pos in |- *; case (Req_EM_T r (RND_Min_Pos r)); intros H1. fold FtoRradix in |- *; intros f H2 H3; rewrite <- H1; auto with real. fold FtoRradix in |- *; intros f H2 H3. case H3; intros V. case (Rle_or_lt (FSucc b radix p (RND_Min_Pos r)) f); auto; intros H4. absurd (f < f)%R; auto with real. apply Rle_lt_trans with (RND_Min_Pos r). rewrite <- FPredSuc with b radix p (RND_Min_Pos r); auto with zarith. 2: apply RND_Min_Pos_canonic; auto. unfold FtoRradix in |- *; rewrite <- FnormalizeCorrect with radix b p f; auto. apply FPredProp; auto with arith zarith. apply FnormalizeCanonic; auto with zarith. apply FSuccCanonic; auto with zarith; apply RND_Min_Pos_canonic; auto. rewrite FnormalizeCorrect; auto with real. apply Rle_lt_trans with (2 := V). apply RND_Min_Pos_Rle; auto. contradict H1. rewrite V; unfold FtoRradix in |- *; rewrite <- FnormalizeCorrect with radix b p f; auto. fold FtoRradix in |- *; apply sym_eq; apply RND_Min_Pos_projector; auto with zarith. unfold FtoRradix in |- *; rewrite FnormalizeCorrect; fold FtoRradix in |- *; auto with real. apply Rle_trans with r; auto with real. apply FnormalizeCanonic; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz