case mpr =>
  intro (NonzeroWithSign.intro (n : ℕ) (_ : Positive n) (_ : a ≃ -s * coe n))
  show NonzeroWithSign (-a) s
  have : -a ≃ s * coe n := calc
    (-a)            ≃ _ := AA.subst₁ ‹a ≃ -s * coe n›
    (-(-s * coe n)) ≃ _ := AA.scompatL
    (-(-s)) * coe n ≃ _ := AA.substL neg_involutive
    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