proposition: Theorem RoundGeNormal: forall f:float, forall r:R, Closest bo radix r f -> (Fnormal radix bo f) -> (Rabs r <= Rabs f * (1 + powerRZ radix (- precision)))%R.
proof: Proof. intros. apply Rplus_le_reg_l with (-Rabs f)%R. apply Rle_trans with (Rabs r-Rabs f)%R;[right; ring|idtac]. apply Rle_trans with (Rabs f * powerRZ radix (- precision) )%R;[idtac|right; ring]. apply Rle_trans with (Rabs (r-f));[apply Rabs_triang_inv|idtac]. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (Fulp bo radix precision f). unfold FtoRradix; apply ClosestUlp; auto. apply Rle_trans with (Rabs f*powerRZ radix (Z.succ (-precision)))%R. unfold FtoRradix; apply FulpLe2; auto. elim H0; auto. rewrite FcanonicFnormalizeEq; auto with zarith. left; auto. right; unfold Z.succ; rewrite powerRZ_add; auto with real zarith. rewrite powerRZ_1; unfold radix; simpl; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz