proposition: Theorem negligible_poly_num : forall f, polynomial f -> negligible (fun n => f n / expnat 2 n)%rat.
proof: Proof. intuition. unfold polynomial in *. do 3 destruct H. eapply negligible_le. intuition. eapply leRat_terms. eapply H. eapply Nat.le_refl. eapply negligible_eq. eapply negligible_plus. eapply negligible_const_mult. eapply negligible_exp. eapply negligible_const_num. intuition. symmetry. rewrite ratAdd_num. eapply ratAdd_eqRat_compat. rewrite <- ratMult_num_den. eapply eqRat_terms. eauto. assert (posnatToNat (pos expnat 2 n) = posnatToNat (posnatMult (pos 1) (pos expnat 2 n))). unfold natToPosnat, posnatToNat, posnatMult. symmetry. eapply Nat.mul_1_l. eapply H0. eapply eqRat_refl. Qed.
imports: FCF.StdNat FCF.Rat