proposition: Lemma epLe: (Fexp p <=s+1+Fexp x)%Z.
proof: Proof. apply Z.le_trans with (Fexp (Float (Fnum x) (s+1+Fexp x))). 2: simpl; auto with zarith. apply Fcanonic_Rle_Zle with radix b t; auto with zarith. left; auto. elim Nx; intros; left; split; auto with zarith. elim H; intros; split; simpl; auto with zarith. rewrite Rabs_right;[idtac|fold FtoRradix; apply Rle_ge; apply pPos]. rewrite Rabs_right;[idtac|fold FtoRradix; apply Rle_ge]. generalize ClosestMonotone; unfold MonotoneP; intros. unfold FtoRradix; apply H with b (x * (powerRZ radix s + 1))%R (x * (powerRZ radix (s + 1)))%R ; auto with zarith real. apply Rmult_lt_compat_l; auto with real. rewrite powerRZ_add; simpl; ring_simplify (radix*1)%R. apply Rlt_le_trans with (powerRZ radix s * 2%Z)%R. apply Rlt_le_trans with (powerRZ radix s+powerRZ radix s)%R. apply Rplus_lt_compat_l; apply Rle_lt_trans with (powerRZ radix 0)%R; auto with real zarith. apply Rlt_powerRZ; auto with zarith; apply IZR_lt; lia. right; simpl; ring. apply Rmult_le_compat_l; auto with real zarith. apply powerRZ_le; apply IZR_lt; lia. apply IZR_le; lia. apply IZR_neq; lia. replace ((x * powerRZ radix (s + 1)))%R with (FtoRradix (Float (Fnum x) (s + 1 + Fexp x)))%R. unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b); auto. apply ClosestRoundedModeP with t; auto with zarith. elim Fx; intros; split; simpl; auto with zarith. unfold FtoRradix, FtoR; simpl; ring_simplify. rewrite powerRZ_add. ring. apply IZR_neq; lia. apply Rle_trans with (x * powerRZ radix (s + 1))%R; auto with real zarith. apply Rmult_le_pos; auto with real zarith. apply powerRZ_le; apply IZR_lt; lia. unfold FtoRradix, FtoR; simpl;right;ring_simplify. repeat rewrite powerRZ_add; try apply IZR_neq; try lia. ring. Qed.
imports: Reals ZArith List PeanoNat Psatz