proposition: Lemma tclosureP A : A \subset Delta -> transitive (srel (tclosure A)).
proof: Proof. move/tclosure_Delta => /subsetP subs. rewrite /= => j i k /= ijA jkA. move: (subs _ ijA) (subs _ jkA); rewrite 2!inE /= => iltj jltk. move: iltj jltk (ltn_trans iltj jltk); rewrite !ltn_neqAle. move=> /andP[inj _] /andP[jnk _] /andP[ink _]. move: ijA jkA; rewrite !inE /= inj ink jnk /=. exact: connect_trans. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype