proposition: Lemma not_FTZ_ulp_ge_ulp_0: (forall x, (ulp 0 <= ulp x)%R) -> Exp_not_FTZ fexp.
proof: Proof. intros H e. apply generic_format_bpow_inv' with beta. apply generic_format_bpow_ge_ulp_0. replace e with ((e-1)+1)%Z by ring. rewrite <- ulp_bpow. apply H. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop