have notTwo : ¬AA.TwoOfThree (n * m < 1) (n * m ≃ 1) (n * m > 1) :=
  (trichotomy (n * m) 1).atMostOne
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this✝² : Positive (n * m)
left✝ : Positive n
right✝ : Positive m
this✝¹ : n ≥ 1
this✝ : n > 1 ∨ n ≃ 1
h✝ : n > 1
this : 1 < n * m
two : AA.TwoOfThree (n * m < 1) (n * m ≃ 1) (n * m > 1)
⊢ n ≃ 1 ∧ m ≃ 1
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this✝² : Positive (n * m)
left✝ : Positive n
right✝ : Positive m
this✝¹ : n ≥ 1
this✝ : n > 1 ∨ n ≃ 1
h✝ : n > 1
this : 1 < n * m
two : AA.TwoOfThree (n * m < 1) (n * m ≃ 1) (n * m > 1)
notTwo : ¬AA.TwoOfThree (n * m < 1) (n * m ≃ 1) (n * m > 1)
⊢ n ≃ 1 ∧ m ≃ 1