proposition: Lemma acyclic_ut r r' (T: transitive r') : acyclic (r ∪ r') <-> acyclic r /\ irreflexive r' /\ acyclic (r' ⨾ r⁺).
proof: Proof. unfold acyclic; ins; rewrite path_ut2; ins. rewrite irreflexive_union, irreflexive_seqC, !seqA, rt_rt, (rtE r); relsf. rewrite irreflexive_union, <- ct_end, irreflexive_seqC, rtE; relsf. rewrite irreflexive_union; intuition. rewrite ct_begin, seqA; sin_rewrite (rewrite_trans T). by rewrite <- seqA, <- ct_begin. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath