feat(group_theory/subsemigroup/basic): subsemigroups (#12111)
Port over submonoid implementation to a generalization: subsemigroups.
Implement submonoids via extends using old_structure_cmd, since that is
what subsemirings do.
Copy over the attribution from submonoids because the content is almost
unchanged.
The submonoid file hasn't been changed, so no proofs rely on the
subsemigroups proofs.
