a * c ^ n < (n - d)! holds true for sufficiently large n.

theorem FloorSemiring.eventually_mul_pow_lt_factorial_sub {K : Type u_1} [Ring K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] (a c : K) (d : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, a * c ^ n < ↑(n - d).factorial