have : ((n * n : ℕ) : ℤ) ≃ (1 : ℤ) := calc
  ((n * n : ℕ) : ℤ) ≃ _ := AA.compat₂
  (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
b✝ : Positive 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
b✝ : Positive a
n : ℕ
left✝ : Positive n
right✝ : a ≃ coe n
this : coe (n * n) ≃ 1
⊢ a ≃ 1