proposition: Lemma acyclic_via_expand_minus : forall X (r : relation X) (IRR1: irreflexive r) (IRR2: irreflexive ((r ⨾ r \ r) ⨾ r＊)), acyclic r.
proof: Proof. unfold acyclic; ins; rewrite ct_begin. by rewrite seq_rt_absorb_l, irreflexive_union. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath