Identity_of_Monoid_is_Cancellable

import Mathlib.Algebra.Group.Defs

theorem Identity_of_Monoid_is_Cancellable {M : Type _} [Monoid M] : (∀ a b : M, 1 * a = 1 * b → a = b) ∧ (∀ a b : M, a * 1 = b * 1 → a = b) := by sorry