proposition: Lemma acyclic_seqC A (r r' : relation A) : acyclic (r ⨾ r') <-> acyclic (r' ⨾ r).
proof: Proof. unfold acyclic; rewrite clos_trans_rotl. unfold irreflexive, seq; ins; desf; intuition; desf; [|eapply H]; rewrite t_rt_step in *; desf; eauto 10. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath