let m := m'
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
⊢ Euclid (step n) q
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
m : ℕ := m'
⊢ Euclid (step n) q