proposition: Theorem RoundLeNormal: forall f:float, forall r:R, Closest bo radix r f -> (Fnormal radix bo f) -> (Rabs f <= Rabs r / (1 - powerRZ radix (- precision)))%R.
proof: Proof. intros. assert (0 < (1 - powerRZ radix (- precision)))%R. apply Rplus_lt_reg_r with (powerRZ radix (- precision)). ring_simplify. replace 1%R with (powerRZ radix 0); [ auto with real zarith | simpl in |- *; auto ]. apply Rlt_powerRZ; try apply IZR_lt; auto with zarith. apply Rmult_le_reg_l with ((1 - powerRZ radix (- precision)))%R; auto with real. apply Rle_trans with (Rabs r);[idtac|right; field; auto with real]. apply Rplus_le_reg_l with (-Rabs r+Rabs f*powerRZ radix (-precision))%R. apply Rle_trans with (Rabs f-Rabs r)%R;[right; ring|idtac]. apply Rle_trans with (Rabs f * powerRZ radix (- precision) )%R;[idtac|right; ring]. apply Rle_trans with (Rabs (f-r));[apply Rabs_triang_inv|idtac]. replace (f-r)%R with (-(r-f))%R;[rewrite Rabs_Ropp|ring]. 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