proposition: Lemma seq_pow_l r n : r ^^ n ⨾ r ≡ r ⨾ r ^^ n.
proof: Proof. induction n; ins; autorewrite with hahn; try done. by rewrite IHn at 1; rewrite seqA. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets