proposition: Lemma semiregular_sym H K : semiregular K H -> semiregular H K.
proof: Proof. move=> regH x /setD1P[ntx Kx]; apply: contraNeq ntx. rewrite -subG1 -setD_eq0 -setIDAC => /set0Pn[y /setIP[Hy cxy]]. by rewrite (sameP eqP set1gP) -(regH y Hy) inE Kx cent1C. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm action quotient gproduct cyclic center) mathcomp(pgroup nilpotent sylow hall abelian)