proposition: Lemma generic_format_bpow_ge_ulp_0 : forall e, (ulp 0 <= bpow e)%R -> F (bpow e).
proof: Proof. intros e; unfold ulp. rewrite Req_bool_true; trivial. case negligible_exp_spec. intros H1 _. apply generic_format_bpow. specialize (H1 (e+1)%Z); lia. intros n H1 H2. apply generic_format_bpow. case (Zle_or_lt (e+1) (fexp (e+1))); intros H4. absurd (e+1 <= e)%Z. lia. apply Z.le_trans with (1:=H4). replace (fexp (e+1)) with (fexp n). now apply le_bpow with beta. now apply fexp_negligible_exp_eq. lia. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop