calc
  a * b ≃ _ := AA.substR ‹b ≃ 1›
  a * 1 ≃ _ := AA.identR
  a     ≃ _ := ‹a ≃ -1›
  (-1)  ≃ _ := Rel.refl
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝ : a ≄ b
a_cases : a ≃ 1 ∨ a ≃ -1
b_cases : b ≃ 1 ∨ b ≃ -1
h✝¹ : a ≃ -1
h✝ : b ≃ 1
⊢ a * b ≃ -1
no goals