have h0mk : 0 < m - k := by exact Nat.sub_pos_of_lt <| Nat.lt_of_le_of_ne hkm hkeqm
case neg
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
h1 : q ^ k - 1 ∣ q ^ (m - k) - 1
hmk : m - k < m
⊢ k ∣ m
case neg
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
h1 : q ^ k - 1 ∣ q ^ (m - k) - 1
hmk : m - k < m
h0mk : 0 < m - k
⊢ k ∣ m