calc
  a * b ≃ _ := AA.substL ‹a ≃ b›
  b * b ≃ _ := ‹Sqrt1 b›.elim
  1     ≃ _ := Rel.refl
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
left✝ : Sqrt1 b
right✝ : a ≃ b
⊢ a * b ≃ 1
no goals