proposition: Lemma has_finite_antichainsI A s (r : relation A) n : n_total s r n -> has_finite_antichains s r.
proof: Proof. vauto. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom