fact: Definition has_finite_antichains A (s : A -> Prop) (r : relation A) := exists n, n_total s r n.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom