proposition: Lemma fexp_negligible_exp_eq: forall n m, (n <= fexp n)%Z -> (m <= fexp m)%Z -> fexp n = fexp m.
proof: Proof. intros n m Hn Hm. case (Zle_or_lt n m); intros H. apply valid_exp; lia. apply sym_eq, valid_exp; lia. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop