proposition: Theorem negligible_const_num : forall k, negligible (fun n => k / expnat 2 n)%rat.
proof: Proof. intuition. eapply negligible_eq. eapply (@negligible_const_mult k (pos 1)). eapply negligible_exp_den. intuition. rewrite <- ratMult_num_den. eapply eqRat_terms. eapply Nat.mul_1_r. unfold natToPosnat, posnatToNat, posnatMult. eapply Nat.mul_1_l. Qed.
imports: FCF.StdNat FCF.Rat