proposition: Lemma ct_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 (S i).
proof: Proof. split. 2: apply inclusion_bunion_l; ins. 2: by rewrite ct_end, pow_rt. apply inclusion_t_ind_right. { exists 0; split; [|by apply pow_1]. destruct n; try lia. forward eapply (TOT (x :: nil)); ins; desf; eauto. } relsf. apply inclusion_bunion_l; intros. rewrite <- Nat.le_succ_l in H. rewrite pow_seq. destruct (eqP (S x) (2 * n)) as [->|]. eapply pow_bounded_n_total; eauto. by apply irreflexive_bunion; intros; rewrite pow_ct. by apply inclusion_bunion_r with (S x); try lia. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom