proposition: Lemma ct_seq_swap r r' : (r ⨾ r')⁺ ⨾ r ≡ r ⨾ (r' ⨾ r)⁺.
proof: Proof. split. { apply ct_ind_left with (P := fun x => x ⨾ _); auto with hahn; ins; rewrite seqA; eauto with hahn. rewrite ct_begin, H, ?seqA; eauto with hahn. } apply ct_ind_right with (P := fun x => _ ⨾ x); auto with hahn; ins; rewrite <- seqA; eauto with hahn. rewrite ct_end, H, <- ?seqA; eauto with hahn. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets