fact: Definition T (x y : nat * nat) : Prop := (fst x = snd y /\ snd x < snd y) \/ (fst x = snd y /\ snd x < fst y).
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)