proposition: Theorem ClosestSuccPred: (Fcanonic radix b f) -> (Rabs(z-f) <= Rabs(z-(FSucc b radix p f)))%R -> (Rabs(z-f) <= Rabs(z-(FPred b radix p f)))%R -> Closest b radix z f.
proof: Proof. intros G; intros; unfold Closest; split; auto. intros g H1; fold FtoRradix. cut ((FPred b radix p f) <= z)%R; [intros T1|idtac]. cut (z <= (FSucc b radix p f))%R; [intros T2|idtac]. case (Rle_or_lt g (FPred b radix p f)); intros. apply Rle_trans with (Rabs (z - f)). rewrite <- Rabs_Ropp; auto with real. replace (- (f - z))%R with (z - f)%R; auto with real. apply Rle_trans with (Rabs (z - FPred b radix p f)); auto with real. rewrite Rabs_right. rewrite Rabs_left1; auto with real. apply Rplus_le_reg_l with (-z)%R. ring_simplify. auto with real. apply Rplus_le_reg_l with z. ring_simplify. apply Rle_trans with (1:=H2); auto with real. apply Rle_ge; auto with real. apply Rplus_le_reg_l with (FPred b radix p f)%R. apply Rle_trans with (FPred b radix p f)%R; auto with real. apply Rle_trans with z; auto with real. cut (f <= g)%R;[intros|idtac]. case H3; intros. cut (FSucc b radix p f <= g)%R;[intros|idtac]. apply Rle_trans with (Rabs (z - f)). rewrite <- Rabs_Ropp; auto with real. replace (- (f - z))%R with (z - f)%R; auto with real. apply Rle_trans with (1:=H). rewrite Rabs_left1. rewrite Rabs_right. apply Rle_trans with ((FSucc b radix p f)-z)%R; auto with real. unfold Rminus; auto with real. apply Rle_ge; apply Rplus_le_reg_l with z. apply Rle_trans with z; auto with real. apply Rle_trans with (FSucc b radix p f)%R; auto with real. apply Rle_trans with g; auto with real. apply Rplus_le_reg_l with (FSucc b radix p f); apply Rle_trans with z; auto with real. apply Rle_trans with (1:=T2); auto with real. apply Rle_trans with (FNSucc b radix p f). right; unfold FNSucc; rewrite FcanonicFnormalizeEq; auto with zarith. unfold FtoRradix; apply FNSuccProp; auto with zarith. rewrite H4; auto with real. replace f with (FNSucc b radix p (FPred b radix p f)). unfold FtoRradix; apply FNSuccProp; auto with zarith. apply FBoundedPred; auto with zarith. unfold FNSucc; rewrite FcanonicFnormalizeEq; auto with zarith. apply FSucPred; auto with zarith. apply FPredCanonic;auto with zarith. case (Rle_or_lt z (FSucc b radix p f)); auto; intros. contradict H; apply Rlt_not_le. rewrite Rabs_right;[idtac|apply Rle_ge]. rewrite Rabs_right;[idtac|apply Rle_ge]. cut (f < (FSucc b radix p f))%R. intros; unfold Rminus; auto with real. unfold FtoRradix; apply FSuccLt; auto with zarith. apply Rplus_le_reg_l with f. apply Rle_trans with f; auto with real; apply Rle_trans with (FSucc b radix p f). apply Rlt_le; unfold FtoRradix; apply FSuccLt; auto with zarith. apply Rlt_le; apply Rlt_le_trans with (1:=H2); auto with real. apply Rle_trans with (z-z)%R; auto with real; unfold Rminus; auto with real. case (Rle_or_lt (FPred b radix p f) z); auto; intros. contradict H0; apply Rlt_not_le. cut ((FPred b radix p f) < f)%R. intros; rewrite Rabs_left1. rewrite Rabs_left1. unfold Rminus; auto with real. apply Rplus_le_reg_l with f. apply Rle_trans with z; auto with real; apply Rlt_le. apply Rlt_trans with (1:=H2); apply Rlt_le_trans with (1:=H0); auto with real. apply Rle_trans with (z-z)%R; auto with real; unfold Rminus; auto with real. unfold FtoRradix; apply FPredLt; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz