proposition: Lemma not_FTZ_generic_format_ulp : (forall x, F (ulp x)) -> Exp_not_FTZ fexp.
proof: Proof. intros H e. specialize (H (bpow (e-1))). rewrite ulp_neq_0 in H. 2: apply Rgt_not_eq, bpow_gt_0. unfold cexp in H. rewrite mag_bpow in H. apply generic_format_bpow_inv' in H. now replace (e-1+1)%Z with e in H by ring. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop