proposition: Lemma pow_rt (n : nat) A (r: relation A) : r^^n ⊆ r＊.
proof: Proof. induction n; simpl; auto with hahn. rewrite IHn, <- ct_end; auto with hahn. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets