apply Natural.ind_on (motive := λ n => Euclid n q) n
n q : ℕ
x✝ : Positive q
this : 0 < q
⊢ Euclid n q
case zero
n q : ℕ
x✝ : Positive q
this : 0 < q
⊢ Euclid 0 q

case step
n q : ℕ
x✝ : Positive q
this : 0 < q
⊢ ∀ (m : ℕ), Euclid m q → Euclid (step m) q