have : (a * b) * (a * b) ≃ 1 := calc
  (a * b) * (a * b) ≃ _ := AA.substL ‹a * b ≃ 1›
  1 * (a * b)       ≃ _ := AA.identL
  a * b             ≃ _ := ‹a * b ≃ 1›
  1                 ≃ _ := Rel.refl
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 1
⊢ Sqrt1 b ∧ a ≃ b
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 1
this : a * b * (a * b) ≃ 1
⊢ Sqrt1 b ∧ a ≃ b