case zero =>
  show Euclid 0 q
  let m := 0
  let r := 0
  have r_bounded : r < q := ‹0 < q›
  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
  exact Euclid.intro m r r_bounded n_divided
n q : ℕ
x✝ : Positive q
this : 0 < q
⊢ Euclid 0 q
no goals