proposition: Lemma Fm: generic_format beta fexpe m.
proof: Proof. case (d_ge_0); intros Y. destruct m_eq as (g,(Hg1,Hg2)); trivial. apply generic_format_F2R' with g. now apply sym_eq. intros H; unfold cexp; rewrite Hg2. rewrite mag_m; trivial. rewrite <- Fexp_d; trivial. rewrite Cd. unfold cexp. generalize (fexpe_fexp (mag beta (F2R d))). lia. destruct m_eq_0 as (g,(Hg1,Hg2)); trivial. apply generic_format_F2R' with g. assumption. intros H; unfold cexp; rewrite Hg2. rewrite mag_m_0; try assumption. apply Z.le_trans with (1:=fexpe_fexp _). generalize (fexp_m_eq_0 Y). lia. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations