calc
  n * m ≃ _ := AA.substL ‹n ≃ 1›
  1 * m ≃ _ := AA.identL
  m     ≃ _ := ‹m ≃ 1›
  1     ≃ _ := Rel.refl
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
left✝ : n ≃ 1
right✝ : m ≃ 1
⊢ n * m ≃ 1
no goals