Cancellable_Elements_of_Monoid_form_Submonoid

import Mathlib.Algebra.Group.Submonoid.Basic

theorem Cancellable_Elements_of_Monoid_form_Submonoid {M : Type _} [Monoid M] : ∃ S : Submonoid M, ∀ x : M, x ∈ S ↔ (∀ a b : M, x * a = x * b → a = b) ∧ (∀ a b : M, a * x = b * x → a = b) := by sorry