proposition: Theorem generic_format_bpow' : forall e, (fexp e <= e)%Z -> generic_format (bpow e).
proof: Proof. intros e He. apply generic_format_bpow. destruct (Zle_lt_or_eq _ _ He). now apply valid_exp_. rewrite <- H. apply valid_exp. rewrite H. apply Z.le_refl. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop