have n_divided : 0 ≃ m * q + r := calc
  0         ≃ _ := Rel.symm Natural.zero_mul
  0 * q     ≃ _ := Rel.symm Natural.add_zero
  0 * q + 0 ≃ _ := Rel.refl
  m * q + r ≃ _ := Rel.refl
n q : ℕ
x✝ : Positive q
this : 0 < q
m : Nat := 0
r : Nat := 0
r_bounded : r < q
⊢ Euclid 0 q
n q : ℕ
x✝ : Positive q
this : 0 < q
m : Nat := 0
r : Nat := 0
r_bounded : r < q
n_divided : 0 ≃ m * q + r
⊢ Euclid 0 q