proposition: Lemma acyclic_union A (r r': relation A) (R: acyclic r) (FF: acyclic (r' ⨾ r＊)): acyclic (r ∪ r').
proof: Proof. unfold acyclic; ins; rewrite path_union. apply irreflexive_union; split; auto. rewrite irreflexive_seqC. rewrite ct_begin, !seqA; relsf. rewrite <- seqA; rewrite <- ct_begin. by rewrite acyclic_seqC in FF. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath