Invertible_Element_of_Associative_Structure_is_Cancellable

import Mathlib.Algebra.Group.Units.Basic

theorem Invertible_Element_of_Associative_Structure_is_Cancellable {M : Type _} [Monoid M] (a : M) (ha : IsUnit a) : (∀ x y : M, a * x = a * y → x = y) ∧ (∀ x y : M, x * a = y * a → x = y) := by sorry