Add proofs for MoufangLoop

[Akshobhya1234]

In this PR

• Correct definitions LeftBol and IsMoufangLoop Show the following for MoufangLoop
• leftAlternative : LeftAlternative _∙_
• rightAlternative : RightAlternative _∙_
• alternative : Alternative _∙_
• z∙xzy≈zxz∙y : ∀ x y z → (z ∙ (x ∙ (z ∙ y))) ≈ (((z ∙ x) ∙ z) ∙ y)
• x∙zyz≈xzy∙z : ∀ x y z → (x ∙ (z ∙ (y ∙ z))) ≈ (((x ∙ z) ∙ y) ∙ z)