have : a * a ≃ (n * n : ℕ) := calc
  a * a               ≃ _ := AA.substL ‹a ≃ sa * n›
  (sa * n) * a        ≃ _ := AA.substR ‹a ≃ sa * n›
  (sa * n) * (sa * n) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (sa * sa) * (n * n) ≃ _ := AA.substL ‹Sqrt1 sa›.elim
  (1 : ℤ) * (n * n)   ≃ _ := AA.identL
  (n : ℤ) * n         ≃ _ := Rel.symm AA.compat₂
  ((n * n : ℕ) : ℤ)   ≃ _ := Rel.refl
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
sa : ℤ
sqrt1✝ : Sqrt1 sa
nws : NonzeroWithSign a sa
n : ℕ
pos✝ : Positive n
eqv✝ : a ≃ sa * coe n
⊢ ∃ n, Positive n ∧ a * a ≃ coe (n * n)
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
sa : ℤ
sqrt1✝ : Sqrt1 sa
nws : NonzeroWithSign a sa
n : ℕ
pos✝ : Positive n
eqv✝ : a ≃ sa * coe n
this : a * a ≃ coe (n * n)
⊢ ∃ n, Positive n ∧ a * a ≃ coe (n * n)