have : ((n * n : ℕ) : ℤ) ≃ (1 : ℤ) := calc
  ((n * n : ℕ) : ℤ)         ≃ _ := AA.compat₂
  (n : ℤ) * (n : ℤ)         ≃ _ := Rel.symm neg_involutive
  (-(-((n : ℤ) * (n : ℤ)))) ≃ _ := AA.subst₁ AA.scompatR
  (-((n : ℤ) * -(n : ℤ)))   ≃ _ := AA.scompatL
  (-(n : ℤ)) * (-(n : ℤ))   ≃ _ := AA.substL (Rel.symm ‹a ≃ -(n : ℤ)›)
  a * (-(n : ℤ))            ≃ _ := AA.substR (Rel.symm ‹a ≃ -(n : ℤ)›)
  a * a                     ≃ _ := ‹Sqrt1 a›.elim
  1                         ≃ _ := Rel.refl
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
n : ℕ
left✝ : Positive n
right✝ : a ≃ -coe n
⊢ a ≃ -1
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
n : ℕ
left✝ : Positive n
right✝ : a ≃ -coe n
this : coe (n * n) ≃ 1
⊢ a ≃ -1