proposition: Lemma generic_format_succ_aux1 : forall x, (0 < x)%R -> F x -> F (x + ulp x).
proof: Proof. intros x Zx Fx. destruct (mag beta x) as (ex, Ex). specialize (Ex (Rgt_not_eq _ _ Zx)). assert (Ex' := Ex). rewrite Rabs_pos_eq in Ex'. destruct (id_p_ulp_le_bpow x ex) ; try easy. unfold generic_format, scaled_mantissa, cexp. rewrite mag_unique with beta (x + ulp x)%R ex. pattern x at 1 3 ; rewrite Fx. rewrite ulp_neq_0. unfold scaled_mantissa. rewrite cexp_fexp with (1 := Ex). unfold F2R. simpl. rewrite Rmult_plus_distr_r. rewrite Rmult_assoc. rewrite <- bpow_plus, Zplus_opp_r, Rmult_1_r. change (bpow 0) with 1%R. rewrite <- plus_IZR. rewrite Ztrunc_IZR. rewrite plus_IZR. rewrite Rmult_plus_distr_r. now rewrite Rmult_1_l. now apply Rgt_not_eq. rewrite Rabs_pos_eq. split. apply Rle_trans with (1 := proj1 Ex'). pattern x at 1 ; rewrite <- Rplus_0_r. apply Rplus_le_compat_l. apply ulp_ge_0. exact H. apply Rplus_le_le_0_compat. now apply Rlt_le. apply ulp_ge_0. rewrite H. apply generic_format_bpow. apply valid_exp. destruct (Zle_or_lt ex (fexp ex)) ; trivial. elim Rlt_not_le with (1 := Zx). rewrite Fx. replace (Ztrunc (scaled_mantissa beta fexp x)) with Z0. rewrite F2R_0. apply Rle_refl. unfold scaled_mantissa. rewrite cexp_fexp with (1 := Ex). destruct (mantissa_small_pos beta fexp x ex) ; trivial. rewrite Ztrunc_floor. apply sym_eq. apply Zfloor_imp. split. now apply Rlt_le. exact H2. now apply Rlt_le. now apply Rlt_le. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop