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

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