have r_bounded : r < q := ‹0 < q›
n q : ℕ
x✝ : Positive q
this : 0 < q
m : Nat := 0
r : Nat := 0
⊢ Euclid 0 q
n q : ℕ
x✝ : Positive q
this : 0 < q
m : Nat := 0
r : Nat := 0
r_bounded : r < q
⊢ Euclid 0 q