proposition: Lemma acyclic_seqC A (r r' : relation A) : acyclic (r ⨾ r') <-> acyclic (r' ⨾ r).
proof: Proof. by unfold acyclic; rewrite ct_rotl, irreflexive_seqC, !seqA, <- ct_end. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets