case zero =>
  show 0 + m ≃ m + 0
  calc
    0 + m ≃ _ := Addition.zero_add
    m     ≃ _ := Rel.symm add_zero
    m + 0 ≃ _ := Rel.refl
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ 0 + m ≃ m + 0
no goals