proposition: Lemma ClosestRoundeGeNormal: forall (z : R) (f : float), Closest bo radix z f -> Fnormal radix bo f -> (Rabs z <= (Rabs f) * Unplus)%R.
proof: Proof. intros. apply Rplus_le_reg_l with (-(Rabs f))%R. apply Rle_trans with (Rabs z-Rabs f)%R;[right; ring|idtac]. apply Rle_trans with (Rabs (z-f));[apply Rabs_triang_inv|idtac]. apply Rle_trans with (Rabs (f) * (/ S 1 * powerRZ radix (Z.succ (- p))))%R. unfold FtoRradix; apply ClosestErrorBoundNormal with bo; auto with zarith. rewrite FcanonicFnormalizeEq; auto with zarith; left; auto. unfold Unplus; simpl; unfold Rdiv; right; field. Qed.
imports: Reals ZArith List PeanoNat Psatz