proposition: Lemma ulp_succ_pos : forall x, F x -> (0 < x)%R -> ulp (succ x) = ulp x \/ succ x = bpow (mag beta x).
proof: Proof. Proof with auto with typeclass_instances. intros x Fx Hx. generalize (Rlt_le _ _ Hx); intros Hx'. rewrite succ_eq_pos;[idtac|now left]. destruct (mag beta x) as (e,He); simpl. rewrite Rabs_pos_eq in He; try easy. specialize (He (Rgt_not_eq _ _ Hx)). assert (H:(x+ulp x <= bpow e)%R). apply id_p_ulp_le_bpow; try assumption. apply He. destruct H;[left|now right]. rewrite ulp_neq_0 at 1. 2: apply Rgt_not_eq, Rgt_lt, Rlt_le_trans with x... 2: rewrite <- (Rplus_0_r x) at 1; apply Rplus_le_compat_l. 2: apply ulp_ge_0. rewrite ulp_neq_0 at 2. 2: now apply Rgt_not_eq. f_equal; unfold cexp; f_equal. apply trans_eq with e. apply mag_unique_pos; split; try assumption. apply Rle_trans with (1:=proj1 He). rewrite <- (Rplus_0_r x) at 1; apply Rplus_le_compat_l. apply ulp_ge_0. now apply sym_eq, mag_unique_pos. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop