proposition: Lemma tclosure_Delta A : A \subset Delta -> tclosure A \subset Delta.
proof: Proof. move/tclosure_sub; apply => j k i; rewrite /= !mem_Delta. exact: ltn_trans. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype