dsimp [Lexcomb]
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬(r a b ∨ Incomp r a b ∧ s a b) ∧ ¬(r b a ∨ Incomp r b a ∧ s b a)