feat(group_theory/sylow): Frattini's Argument (#9662)
Frattini's argument: If `N` is a normal subgroup of `G`, and `P` is a Sylow `p`-subgroup of `N`, then `PN=G`.
The proof is an application of Sylow's second theorem (all Sylow `p`-subgroups of `N` are conjugate).
