Existence of a sufficiently large prime for which a * c ^ p / (p - 1)! < 1

This is a technical result used in the proof of the Lindemann-Weierstrass theorem.

theorem FloorRing.exists_prime_mul_pow_lt_factorial {K : Type u_1} [LinearOrderedRing K] [FloorRing K] (n : ℕ) (a : K) (c : K) : ∃ p > n, Nat.Prime p ∧ a * c ^ p < ↑(p - 1).factorial

theorem FloorRing.exists_prime_mul_pow_div_factorial_lt_one {K : Type u_1} [LinearOrderedField K] [FloorRing K] (n : ℕ) (a : K) (c : K) : ∃ p > n, Nat.Prime p ∧ a * c ^ p / ↑(p - 1).factorial < 1