proposition: Lemma acyclic_seq_via_expand_minus : forall X (r r' : relation X) (IRR1: irreflexive (r ⨾ r')) (IRR2: irreflexive ((r ⨾ r' ⨾ r \ r) ⨾ r' ⨾ (r ⨾ r')＊)), acyclic (r ⨾ r').
proof: Proof. unfold acyclic; ins; rewrite ct_end, <- seqA. rewrite seq_rt_absorb_r, !seqA; relsf. rewrite irreflexive_union; split; ins. by rewrite seqA, irreflexive_seqC, seqA. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath