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