fact: Definition n_total A (s : A -> Prop) (r : relation A) (n : nat) := forall l (LLEN: n < length l) (ND: NoDup l) (INCL: forall x, In x l -> s x), exists a b, a <> b /\ In a l /\ In b l /\ r a b.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom