proposition: Lemma maximal_eqJ x : maximal_eq (G :^ x) (H :^ x) = maximal_eq G H.
proof: Proof. by rewrite /maximal_eq !eqEsubset !conjSg maximalJ. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)