proposition: Lemma generic_format_ulp : Exp_not_FTZ fexp -> forall x, F (ulp x).
proof: Proof. unfold Exp_not_FTZ; intros H x. case (Req_dec x 0); intros Hx. rewrite Hx; apply generic_format_ulp_0. rewrite (ulp_neq_0 _ Hx). apply generic_format_bpow. apply H. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop