case mpr =>
  intro (_ : sgn a ≄ sgn b)
  show Negative (a * b)
  have (And.intro (_ : Sqrt1 (sgn a)) (_ : Sqrt1 (sgn b))) :=
    sqrt1_sgn_split_nonzero_mul ‹Nonzero (a * b)›
  have nws_ab : NonzeroWithSign (a * b) (sgn a * sgn b) :=
    nonzeroWithSign_mul_from_sqrt1_sgn
  have : sgn a * sgn b ≃ -1 := mul_sqrt1_neqv.mpr ‹sgn a ≄ sgn b›
  have : NonzeroWithSign (a * b) (-1) :=
    NonzeroWithSign.subst_sign this nws_ab
  have : Negative (a * b) := negative_iff_sign_neg1.mpr this
  exact this
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a b : ℤ
inst✝ : Nonzero (a * b)
⊢ sgn a ≄ sgn b → Negative (a * b)
no goals