case zero =>
  show 0 * (m + k) ≃ 0 * m + 0 * k
  calc
    0 * (m + k)   ≃ _ := zero_mul
    0             ≃ _ := Rel.symm Addition.zero_add
    0 + 0         ≃ _ := AA.substL (Rel.symm zero_mul)
    0 * m + 0     ≃ _ := AA.substR (Rel.symm zero_mul)
    0 * m + 0 * k ≃ _ := Rel.refl
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m k : ℕ
⊢ 0 * (m + k) ≃ 0 * m + 0 * k
no goals