proposition: Lemma acyclic_specific_absorb A (r r' : relation A) : r ⨾ r' ⊆ r ⨾ r -> r' ⨾ r' ⊆ r' ⨾ r -> acyclic r -> irreflexive r' -> acyclic (r ∪ r').
proof: Proof. ins. red. rewrite path_specific_absorb; try done. apply irreflexive_union; split; try done. rewrite irreflexive_seqC. rewrite rtE; relsf. apply irreflexive_union; split; try done. by rewrite ct_end, seqA, H, <- seqA, <- ct_end, ct_unit. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath