proposition: Lemma pow_S_begin A (r : relation A) n : r^^(S n) ≡ r ⨾ r^^n.
proof: Proof. induction n; ins; rewrite ?seq_id_l, ?seq_id_r; ins. by rewrite IHn at 1; rewrite seqA. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets