proposition: Lemma negligible_exp_spec': (negligible_exp = None /\ forall n, (fexp n < n)%Z) \/ exists n, (negligible_exp = Some n /\ (n <= fexp n)%Z).
proof: Proof. unfold negligible_exp; destruct LPO_Z as [(n,Hn)|Hn]. right; simpl; exists n; now split. left; split; trivial. intros n; specialize (Hn n); lia. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop