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