introduce subgroup inclusions and equality

[Alizter]

We should introduce subgroup inclusions and subgroup equality (based on iff) like we have done for ideals. In fact, we could probably just move the ideal versions to Subgroup.v. It is used in quite a few places implicitly already, so we will have to go through and change them where it makes sense to do so.