proposition: Lemma generic_format_fexpe_fexp: forall x, generic_format beta fexp x -> generic_format beta fexpe x.
proof: Proof. intros x Hx. apply generic_inclusion_mag with fexp; trivial; intros Hx2. generalize (fexpe_fexp (mag beta x)). lia. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations