proposition: Lemma acyclic_union_total_l r dom r' (T: is_total dom r) (DB: domb r dom) : acyclic (r ∪ r') <-> acyclic r /\ acyclic r' /\ irreflexive (r⁺ ⨾ r'⁺).
proof: Proof. rewrite unionC, irreflexive_seqC, acyclic_union_total_r; eauto; tauto. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath