case mp =>
  intro (NonzeroWithSign.intro (n : ℕ) (_ : Positive n) (_ : -a ≃ s * coe n))
  show NonzeroWithSign a (-s)
  have : a ≃ -s * coe n := calc
    a              ≃ _ := Rel.symm neg_involutive
    (-(-a))        ≃ _ := AA.subst₁ ‹-a ≃ s * coe n›
    (-(s * coe n)) ≃ _ := AA.scompatL
    (-s) * coe n   ≃ _ := Rel.refl
  exact NonzeroWithSign.intro n ‹Positive n› ‹a ≃ -s * coe n›
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
⊢ NonzeroWithSign (-a) s → NonzeroWithSign a (-s)
no goals