∀ {S : Type u_1} [inst : CommRing S] {P : Ideal S} [P_prime : P.IsPrime] [IsDedekindDomain S],
  P ≠ ⊥ →
    ∀ {i : ℕ} (a d d' e e' : S),
      a ∉ P ^ (i + 1) → e ∈ P ^ (i + 1) → e' ∈ P ^ (i + 1) → a * d + e - (a * d' + e') ∈ P ^ (i + 1) → d - d' ∈ P