rcases hso with ⟨_, (⟨_, _, heq⟩ | ⟨_, hdvd3, _⟩ | ⟨hdvd2, _, _⟩)⟩
hso : (R3 2 3 → R3 3 1 → R3 2 1) ∧ Trichotomy (R3 2 3) (R3 3 2) (2 = 3)
⊢ False
case intro.inl.intro.intro
left✝² : R3 2 3 → R3 3 1 → R3 2 1
left✝¹ : ¬R3 2 3
left✝ : ¬R3 3 2
heq : 2 = 3
⊢ False

case intro.inr.inl.intro.intro
left✝¹ : R3 2 3 → R3 3 1 → R3 2 1
left✝ : ¬R3 2 3
hdvd3 : R3 3 2
right✝ : ¬2 = 3
⊢ False

case intro.inr.inr.intro.intro
left✝¹ : R3 2 3 → R3 3 1 → R3 2 1
hdvd2 : R3 2 3
left✝ : ¬R3 3 2
right✝ : ¬2 = 3
⊢ False