proposition: Theorem succ_eq_pos : forall x, (0 <= x)%R -> succ x = (x + ulp x)%R.
proof: Proof. intros x Hx; unfold succ. now rewrite Rle_bool_true. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop