case zero =>
  intro (_ : 0 + m ≃ 0 + k)
  show m ≃ k
  calc
    m     ≃ _ := Rel.symm Addition.zero_add
    0 + m ≃ _ := ‹0 + m ≃ 0 + k›
    0 + k ≃ _ := Addition.zero_add
    k     ≃ _ := Rel.refl
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m k : ℕ
⊢ 0 + m ≃ 0 + k → m ≃ k
no goals