proposition: Theorem negligible_exp_den : negligible (fun n => 1 / expnat 2 n)%rat.
proof: Proof. unfold negligible in *. intuition. destruct (poly_lt_exp c). exists x. intuition. eapply (rat_num_not_le). eapply H1. unfold posnatToNat, natToPosnat. eapply H. lia. Qed.
imports: FCF.StdNat FCF.Rat