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 : ℕ
x✝ : 0 + m ≃ 0 + k
⊢ m ≃ k
no goals