proposition: Lemma tclosure_sub A B : A \subset B -> transitive (srel B) -> tclosure A \subset B.
proof: Proof. move=> /subsetP AB trB. apply/subsetP => /= [[i j]]; rewrite /tclosure inE /= => /andP[Hneq]. move/connectP => /= [p]; elim: p => [| p0 p IHp] /= in i Hneq *. by move=> _ Heq; rewrite Heq eqxx in Hneq. case: (p0 =P j) => [<- /= /andP[/AB ->] // | /eqP {}/IHp IHp]. by move=> /andP[/AB {}/trB trB {}/IHp /[apply]]; apply: trB. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr