proposition: Lemma negligible_le : forall f1 f2, (forall n, f2 n <= f1 n)%rat -> negligible f1 -> negligible f2.
proof: Proof. intuition. unfold negligible in *. intuition. edestruct H0. econstructor. intuition. eapply H1. eauto. rewrite H3. eauto. Qed.
imports: FCF.StdNat FCF.Rat