case mp =>
  intro (_ : a * b ≃ -1) (_ : a ≃ b)
  show False
  have : (-1 : ℤ) ≃ 1 := calc
    (-1 : ℤ) ≃ _ := Rel.symm ‹a * b ≃ -1›
    a * b    ≃ _ := AA.substL ‹a ≃ b›
    b * b    ≃ _ := ‹Sqrt1 b›.elim
    1        ≃ _ := Rel.refl
  have : (-1 : ℤ) ≄ 1 := neg_one_neqv_one
  exact absurd ‹(-1 : ℤ) ≃ 1› ‹(-1 : ℤ) ≄ 1›
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
⊢ a * b ≃ -1 → a ≄ b
no goals