proposition: Lemma ClosestRoundeLeNormal: forall (z : R) (f : float), Closest bo radix z f -> Fnormal radix bo f -> (Rabs f <= (Rabs z) / Unmoins)%R.
proof: Proof. intros. generalize UnMoinsPos; intros U1. apply Rmult_le_reg_l with Unmoins; auto with real. apply Rle_trans with (Rabs z);[idtac|right; field; auto with real]. apply Rplus_le_reg_l with (-Rabs z+(1-Unmoins)*Rabs f)%R. apply Rle_trans with (Rabs f-Rabs z)%R;[right; ring|idtac]. apply Rle_trans with (Rabs (f-z));[apply Rabs_triang_inv|idtac]. replace (f-z)%R with (-(z-f))%R;[rewrite Rabs_Ropp|ring]. 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 Unmoins, Rdiv; right; simpl; field. Qed.
imports: Reals ZArith List PeanoNat Psatz