Ping pong lemma!

Stream: maths

[Joachim Breitner]

I just proved the ping-pong lemma for free products of groups! sorry-free, but still lots of cleanup needed. In fact, I might refactor it a lot to avoid list.last etc…. so no PR yet.