Results on Central Groupoids

[b-mehta]

Closes https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Central.20groupoids.

This PR contains a number of results on central groupoids and natural central groupoids.

This is a draft PR.

• Ensure that @zaklogician's work is not destroyed here - probably the simplest way is to move that file to NonnaturalCentralGroupoids.lean
• Give an example of an implication that reduction can disprove
• Add a module doc which more clearly highlights the key results here

[zaklogician]

This is very nice work. Re point 1: would same file but separate namespace be a viable solution? I think it'd avoid cluttering up the main equational_theories directory, and keep everything about central groupoids in one location.

[b-mehta]

Unfortunately not, the imports I need from mathlib clash with some of your results