have hStrich := hS.trich p.1 q.1
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
⊢ Trichotomy (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) (S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) (p = q)
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
hStrich : Trichotomy (S p.1 q.1) (S q.1 p.1) (p.1 = q.1)
⊢ Trichotomy (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) (S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) (p = q)