proposition: Theorem negligible_mult_ident : forall f, negligible f -> negligible (fun x => (x / 1) * (f x))%rat.
proof: Proof. unfold negligible in *. intuition. destruct (H (S c)). exists x. intuition. eapply H0. lia. simpl. assert ( (RatIntro 1 (natToPosnat (expnat_nz (S c) pf_nz))) == RatIntro 1 (posnatMult (pos x0) (pos expnat x0 c)) )%rat. eapply eqRat_terms; trivial. simpl in *. rewrite H3. rewrite ratMult_denom. rewrite H2. rewrite <- ratMult_assoc. rewrite <- ratMult_num_den. rewrite num_dem_same_rat1. rewrite ratMult_1_l. intuition. unfold natToPosnat, posnatToNat, posnatMult. lia. Qed.
imports: FCF.StdNat FCF.Rat