have hic : (i - j).Coprime p := by
  rw [Nat.coprime_comm]; apply Nat.coprime_of_lt_prime _ _ hp
  apply Nat.sub_pos_of_lt hilj
  by_cases hj : 0 < j
  apply lt_trans _ hi
  apply Nat.sub_lt_of_pos_le hj hilj.le
  simp only [not_lt, _root_.le_zero_iff] at hj
  rw [hj]
  simp only [tsub_zero]
  exact hi
case pos
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
⊢ ∃ u, ζ ^ j * (ζ ^ (i - j) - 1) = ↑u * (1 - ζ)

case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : ¬j < i
⊢ ∃ u, ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
case pos
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hic : (i - j).Coprime p
⊢ ∃ u, ζ ^ j * (ζ ^ (i - j) - 1) = ↑u * (1 - ζ)

case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : ¬j < i
⊢ ∃ u, ζ ^ i - ζ ^ j = ↑u * (1 - ζ)