proposition: Theorem negligible_exp : forall z, negligible (fun n => expnat n z / expnat 2 n)%rat.
proof: Proof. induction z; simpl in *; intuition. eapply negligible_exp_den. eapply negligible_eq. eapply negligible_mult_ident. eauto. intuition. rewrite <- ratMult_num_den. eapply eqRat_terms; trivial. unfold posnatToNat, natToPosnat, posnatMult. eapply Nat.mul_1_l. Qed.
imports: FCF.StdNat FCF.Rat