proposition: Theorem pred_plus_ulp : forall x, (0 < x)%R -> F x -> (pred x + ulp (pred x))%R = x.
proof: Proof. intros x Hx Fx. rewrite pred_eq_pos. now apply pred_pos_plus_ulp. now apply Rlt_le. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop