proposition: Lemma perm_onM H s t : perm_on H s -> perm_on H t -> perm_on H (s * t).
proof: Proof. move/subsetP=> sH /subsetP tH; apply/subsetP => x; rewrite inE /= permM. by have [-> /tH | /sH] := eqVneq (s x) x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)