proposition: Lemma acyclic_union1 A (r r': relation A) (R: acyclic r) (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, <- ct_begin. rewrite rtE; relsf. rewrite path_union. apply irreflexive_union; split; auto. rewrite irreflexive_seqC. rewrite ct_begin, !seqA; relsf. rewrite <- !seqA, <- ct_begin. apply acyclic_rotl. rewrite <- seqA, <- ct_begin. by apply acyclic_rotl. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath