proposition: Lemma pow_add A (r : relation A) m n : r^^(m + n) ≡ r^^m ⨾ r^^n.
proof: Proof. induction m; ins; rewrite ?seq_id_l, ?seq_id_r; ins. by rewrite IHm, !seqA, <- pow_S_begin. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets