proposition: Lemma acyclic_absorb A (r r': relation A) (F: r' ⨾ r ⊆ r \/ r' ⨾ r ⊆ r') : acyclic (r ∪ r') <-> acyclic r /\ acyclic r'.
proof: Proof. intuition; eauto 2 using acyclic_mon with hahn. all: unfold acyclic; ins; rewrite path_absorb; eauto. all: rewrite !irreflexive_union; splits; ins. all: apply irreflexive_seqC. * eapply irreflexive_inclusion, H1. eapply ct_ind_right with (P:= fun x => x ;; _); ins; eauto with hahn. all: rewrite ct_begin at 1; rewrite ?seqA; sin_rewrite H; rewrite <- ct_begin; relsf. * eapply irreflexive_inclusion, H2. eapply ct_ind_left with (P:= fun x => _ ;; x); ins; eauto with hahn. all: rewrite ct_end at 1; rewrite ?seqA; sin_rewrite H; seq_rewrite <- ct_end; relsf. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath