proposition: Lemma rt_bounded_n_total A s (r : relation A) (ACYC: acyclic r) (DOMA: doma r s) n (TOT: n_total s r n) : r＊ ≡ ⋃ i <= 2 * n, pow_rel r i.
proof: Proof. split; auto using inclusion_bunion_l, pow_rt. rewrite rtE, ct_bounded_n_total; eauto. repeat (apply inclusion_union_l || apply inclusion_bunion_l; intros). apply inclusion_bunion_r with 0; ins; lia. apply inclusion_bunion_r with (S x); ins. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom