proposition: Theorem RND_Closest_correct : forall r : R, Closest b beta r (RND_Closest r).
proof: Proof. intros r. generalize (radix_gt_1 beta); intros M. split. apply FcanonicBound with beta; apply RND_Closest_canonic. intros f H3; fold FtoRradix. cut (RND_Min b beta p r <= r)%R; [ intros V1 | idtac ]. 2: apply (RND_Min_correct b beta p) with (r:=r); easy. cut (r <= RND_Max b beta p r)%R; [ intros V2 | idtac ]. 2: apply (RND_Max_correct b beta p) with (r:=r); easy. cut (forall v w : R, (v <= w)%R -> (0 <= w - v)%R); [ intros V3 | idtac ]. 2: intros v w H; apply Rplus_le_reg_l with v; ring_simplify; auto with real. cut (forall v w : R, (v <= w)%R -> (v - w <= 0)%R); [ intros V4 | idtac ]. 2: intros v w H; apply Rplus_le_reg_l with w; ring_simplify; auto with real. unfold RND_Closest; case (Rle_dec _ _); intros H1. case (Rle_lt_or_eq_dec _ _ H1); intros H2. rewrite Rabs_right in H1; [ idtac | apply Rle_ge; apply V3; auto with real ]. rewrite Rabs_left1 in H1; [ idtac | apply V4; auto with real ]. rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ]. case (Rle_or_lt f r); intros H4. rewrite Rabs_left1; [ idtac | apply V4; auto with real ]. apply Rle_trans with (1 := H1); apply Ropp_le_contravar; unfold Rminus in |- *; apply Rplus_le_compat_r. apply (RND_Min_correct b beta p) with (r:=r); easy. rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ]. unfold Rminus in |- *; apply Rplus_le_compat_r. apply (RND_Max_correct b beta p) with (r:=r); try easy. now apply Rlt_le. case (choice _). rewrite Rabs_right in H1; [ idtac | apply Rle_ge; apply V3; auto with real ]. rewrite Rabs_left1 in H1; [ idtac | apply V4; auto with real ]. rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ]. case (Rle_or_lt f r); intros H5. rewrite Rabs_left1; [ idtac | apply V4; auto with real ]. apply Rle_trans with (1 := H1); apply Ropp_le_contravar; unfold Rminus in |- *; apply Rplus_le_compat_r. apply (RND_Min_correct b beta p) with (r:=r); easy. rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ]. unfold Rminus in |- *; apply Rplus_le_compat_r. apply (RND_Max_correct b beta p) with (r:=r); try easy. now apply Rlt_le. rewrite Rabs_right in H1; [ idtac | apply Rle_ge; apply V3; auto with real ]. rewrite Rabs_left1 in H1; [ idtac | apply V4; auto with real ]. rewrite <- H2. rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ]. case (Rle_or_lt f r); intros H5. rewrite Rabs_left1; [ idtac | apply V4; auto with real ]. apply Rle_trans with (1 := H1); apply Ropp_le_contravar; unfold Rminus in |- *; apply Rplus_le_compat_r. apply (RND_Min_correct b beta p) with (r:=r); easy. rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ]. unfold Rminus in |- *; apply Rplus_le_compat_r. apply (RND_Max_correct b beta p) with (r:=r); try easy. now apply Rlt_le. apply Rnot_le_lt in H1. rewrite Rabs_left1 in H1; [ idtac | apply V4; auto with real ]. rewrite Rabs_right in H1; [ idtac | apply Rle_ge; apply V3; auto with real ]. rewrite Rabs_left1; [ idtac | apply V4; auto with real ]. case (Rle_or_lt f r); intros H4. rewrite Rabs_left1; [ idtac | apply V4; auto with real ]. apply Ropp_le_contravar, Rplus_le_compat_r. apply (RND_Min_correct b beta p) with (r:=r); easy. rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ]. left; apply Rlt_le_trans with (1:=H1). apply Rplus_le_compat_r. apply (RND_Max_correct b beta p) with (r:=r); try easy. now left. Qed.
imports: Coq(Lia) Pff Core