proposition: Theorem negligible_const_mult : forall (n : nat) d f, negligible f -> negligible (fun x => (RatIntro n d) * (f x))%rat.
proof: Proof. unfold negligible in *. intuition. destruct (eq_nat_dec n 0). subst. exists 1. intuition. assert ((1 / expnat x c) == 0)%rat. eapply leRat_0_eq. rewrite H1. rewrite rat_num_0. rewrite ratMult_0_l. intuition. eapply rat_num_nz; [idtac | eauto]. lia. destruct (H (c + n)). exists (x + n)%nat. intuition. eapply H0. lia. assert (1 / expnat x0 (c + n) == RatIntro 1 (pos (expnat x0 c)) * RatIntro 1 (pos (expnat x0 n)))%rat. rewrite <- ratMult_num_den. eapply eqRat_terms. symmetry. eapply Nat.mul_1_r. unfold natToPosnat, posnatToNat, posnatMult. rewrite expnat_plus. trivial. rewrite H3. rewrite H2. rewrite ratMult_comm. rewrite <- ratMult_assoc. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. rewrite <- ratMult_1_l. eapply eqRat_refl. } eapply ratMult_leRat_compat; intuition. eapply rat_le_1. destruct d. unfold natToPosnat, posnatToNat, posnatMult. rewrite Nat.mul_comm. eapply Nat.mul_le_mono. eapply Nat.le_trans. eapply le_expnat_2. eapply expnat_base_le. lia. lia. Qed.
imports: FCF.StdNat FCF.Rat