proposition: Lemma RleRRounded: forall (f : float) (z : R), Fnormal radix b f -> Closest b radix z f -> (Rabs z <= (Rabs f)*(1+(powerRZ radix (1-t))/2))%R.
proof: Proof. intros. replace z with ((z-f)+f)%R;[idtac|ring]. apply Rle_trans with (Rabs(z-f)+Rabs(f))%R;[apply Rabs_triang|idtac]. apply Rplus_le_reg_l with (- Rabs(f))%R. ring_simplify. apply Rmult_le_reg_l with 2; auto with real zarith. apply Rle_trans with (Fulp b radix t f). unfold FtoRradix; apply ClosestUlp; auto with zarith. apply Rle_trans with (Rabs f * powerRZ radix (Z.succ (- t)))%R. unfold FtoRradix; apply FulpLe2; auto with zarith. elim H; auto. rewrite FcanonicFnormalizeEq; auto with zarith; left; auto. unfold Z.succ; replace (-t+1)%Z with (1-t)%Z;[idtac|ring]. simpl; right; field; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz