have : step r' ≤ q := Natural.lt_step_le.mp ‹r' < q›
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'
⊢ Euclid (step n) q
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
⊢ Euclid (step n) q