Commutators, commutator subgroups and three subgroups lemma

[Alizter]

In this PR we define the commutator of group elements [x, y] := x * y * x^ * y^ and state and prove the basic identities about them.

We also prove the Hall-Witt identity and its variant. This is a Jacobi-like identity for commutators of groups.

Next we show that precomposing the predicate of a normal subgroup with a commutator is itself a subgroup. I couldn't find the name of this idea.

We define the commutator subgroup of two subgroups of a group, and then study the commutator of a group with itself which we call the derived subgroup. We show that it is normal and furthermore the quotient is commutative. We then state and prove that it is an abelianization and therefore automatically isomrophic to our abelianization.

Finally we prove the "three subgroups lemma" which will allow us to simplify arguments with combinators in the future.

I missed the dependency on:

• improvements to trivial group #2186

[jdchristensen]

LGTM after the last fix to the comment.

[Alizter]

I will squash before merging.