Auxiliary lemmas for the second case

Supporting ideal-theoretic and arithmetic lemmas used in the second case of Fermat's Last Theorem.

theorem exists_not_dvd_spanSingleton_eq {R : Type u_2} [CommRing R] [IsDedekindDomain R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] {x : R} (hx : Prime x) (I J : Ideal R) (hI : ¬Ideal.span {x} ∣ I) (hJ : ¬Ideal.span {x} ∣ J) (h : (↑(↑I / ↑J)).IsPrincipal) : ∃ (a : R) (b : R), ¬x ∣ a ∧ ¬x ∣ b ∧ FractionalIdeal.spanSingleton (nonZeroDivisors R) ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J