proposition: Lemma pow_of_transitive_cr (n : nat) A (r: relation A) : transitive r -> r^^n ⊆ r^?.
proof: Proof. by ins; rewrite pow_rt, rt_of_trans. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets