Lemmas for units in an ordered monoid

theorem Units.mulLECancellable_val {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (a : Mˣ) : MulLECancellable ↑a

theorem Units.mul_le_mul_left {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (a : Mˣ) {b c : M} : ↑a * b ≤ ↑a * c ↔ b ≤ c

theorem IsUnit.mulLECancellable {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] {a : M} (ha : IsUnit a) : MulLECancellable a

theorem IsUnit.mul_le_mul_left {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] {a b c : M} (ha : IsUnit a) : a * b ≤ a * c ↔ b ≤ c

theorem Units.mul_le_mul_right {M : Type u_1} [Monoid M] [LE M] [MulRightMono M] (a : Mˣ) {b c : M} : b * ↑a ≤ c * ↑a ↔ b ≤ c

theorem IsUnit.mul_le_mul_right {M : Type u_1} [Monoid M] [LE M] [MulRightMono M] {a b c : M} (ha : IsUnit a) : b * a ≤ c * a ↔ b ≤ c