proposition: Lemma wLe: (Rabs w <= powerRZ radix (Fexp z)*(2*radix+1))%R.
proof: Proof. assert (powerRZ radix (Fexp z) * (2*radix+1)=Float (2*radix+1) (Fexp z))%R. apply trans_eq with (powerRZ radix (Fexp z) * (2 * radix + 1)%Z)%R. rewrite plus_IZR; rewrite mult_IZR; simpl; ring. unfold FtoRradix, FtoR; simpl; ring. rewrite H. unfold FtoRradix; apply RoundAbsMonotoner with bo p (Closest bo radix) (t+v)%R; auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. elim zDef; intros I1 I2; elim I1; intros; split; [idtac|simpl; auto with zarith]. apply Z.le_lt_trans with (Z.abs (2*radix+1)); auto with zarith. rewrite Z.abs_eq; auto with zarith. apply Z.lt_le_trans with (2*radix+radix)%Z; auto with zarith. apply Z.le_trans with (3*radix)%Z; auto with zarith. rewrite pGivesBound; apply Z.le_trans with (Zpower_nat radix 3); auto with zarith. unfold Zpower_nat; simpl (nat_rect _ _ _ _)%Z. rewrite Zmult_comm; apply Zmult_le_compat_l. ring_simplify (radix*1)%Z; apply Z.le_trans with (2*2)%Z. auto with zarith. apply Zmult_le_compat; auto with zarith. auto with zarith. apply Zpower_nat_monotone_le; lia. fold FtoRradix; rewrite <- H. apply Rle_trans with (Rabs t+Rabs v)%R;[apply Rabs_triang|idtac]. generalize tLe; generalize vLe; intros. apply Rle_trans with ( powerRZ radix (Fexp z) * (radix + 1)+powerRZ radix (Fexp z) * radix)%R; [auto with real|right; ring]. Qed.
imports: Reals ZArith List PeanoNat Psatz