proposition: Lemma pred_pos_plus_ulp : forall x, (0 < x)%R -> F x -> (pred_pos x + ulp (pred_pos x) = x)%R.
proof: Proof. intros x Zx Fx. unfold pred_pos. case Req_bool_spec; intros H. case (Req_EM_T (x - bpow (fexp (mag_val beta x (mag beta x) -1))) 0); intros H1. rewrite H1, Rplus_0_l. now apply pred_pos_plus_ulp_aux3. now apply pred_pos_plus_ulp_aux2. now apply pred_pos_plus_ulp_aux1. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop