proposition: Lemma ct_rotl r r' : (r ⨾ r')⁺ ≡ r ⨾ (r' ⨾ r) ＊ ⨾ r'.
proof: Proof. by rewrite rt_seq_swap, ct_begin, seqA. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets