proposition: Lemma negligible_exp_spec: negligible_exp_prop negligible_exp.
proof: Proof. unfold negligible_exp; destruct LPO_Z as [(n,Hn)|Hn]. now apply negligible_Some. apply negligible_None. intros n; specialize (Hn n); lia. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop