proposition: Lemma acyclic_union_total_r 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 acyclic_decomp_u_total; eauto; rewrite rtE; relsf; rewrite irreflexive_union; tauto. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath