proposition: Lemma generic_format_ulp_0 : F (ulp 0).
proof: Proof. unfold ulp. rewrite Req_bool_true; trivial. case negligible_exp_spec. intros _; apply generic_format_0. intros n H1. apply generic_format_bpow. now apply valid_exp. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop