proposition: Lemma pow_ct (n : nat) A (r: relation A) (NZ : n <> 0) : r^^n ⊆ r⁺.
proof: Proof. by destruct n; ins; rewrite pow_rt, ct_end. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets