Existence of a minimal support prime

A nontrivial finite module over a commutative Noetherian ring has a prime in its support which is minimal among the support primes.

theorem AlgebraicAnalysis.MinimalSupportExistence.exists_minimal_support_prime {R : Type u_1} {U : Type u_2} [CommRing R] [AddCommGroup U] [Module R U] [Module.Finite R U] [Nontrivial U] : ∃ q ∈ Module.support R U, ∀ p ∈ Module.support R U, p.asIdeal ≤ q.asIdeal → q.asIdeal ≤ p.asIdeal