proposition: Lemma seq_rtE_r r r' : r ⨾ r' ＊ ≡ r ∪ (r ⨾ r') ⨾ r' ＊.
proof: Proof. by rewrite rt_begin at 1; rewrite ?seq_union_r, ?seq_id_r, ?seqA. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets