proposition: Lemma acyclic_decomp_u_total r dom r' (T: is_total dom r') (DB: domb r' dom) : acyclic (r ∪ r') <-> acyclic r /\ irreflexive (r＊ ⨾ r'⁺).
proof: Proof. split; intuition. by eapply inclusion_acyclic; try eassumption; eauto with hahn. eapply irreflexive_inclusion; try eassumption. by rewrite <- rt_ct with (r := r ∪ r'); eauto with hahn. unfold acyclic; rewrite path_decomp_u_total; eauto. eapply irreflexive_union; splits; ins; rewrite irreflexive_seqC, seqA in *; rels. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath