proposition: Lemma fsupp_ct r (ACYC: acyclic r) s (DOMA: doma r s) (TOT: has_finite_antichains s r) : fsupp r -> fsupp r⁺.
proof: Proof. destruct TOT; intros; rewrite ct_bounded_n_total; eauto using fsupp_bunion, fsupp_pow with hahn. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom