feat(GroupTheory/GroupAction/SubMulAction/Combination): primitivity of the permutation action. (leanprover-community#34307)

Prove the primitivity of the permutation action of `Equiv.Perm` or `alternatingGroup` on `Nat.Combination`.

This will be used in leanprover-community#33082 to prove the simplicity of the alternating group on at least 5 letters.

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: AntoineChambert-Loir