mathlib documentation

algebra.order.monoid_lemmas

Ordered monoids #

This file develops the basics of ordered monoids.

Implementation details #

Unfortunately, the number of ' appended to lemmas in this file may differ between the multiplicative and the additive version of a lemma. The reason is that we did not want to change existing names in the library.

Remark #

Almost no monoid is actually present in this file: most assumptions have been generalized to has_mul or mul_one_class.

theorem mul_le_mul_left' {α : Type u_1} [has_mul α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {b c : α} (bc : b c) (a : α) :
a * b a * c
theorem add_le_add_left {α : Type u_1} [has_add α] [has_le α] [covariant_class α α has_add.add has_le.le] {b c : α} (bc : b c) (a : α) :
a + b a + c
theorem le_of_mul_le_mul_left' {α : Type u_1} [has_mul α] [has_le α] [contravariant_class α α has_mul.mul has_le.le] {a b c : α} (bc : a * b a * c) :
b c
theorem le_of_add_le_add_left {α : Type u_1} [has_add α] [has_le α] [contravariant_class α α has_add.add has_le.le] {a b c : α} (bc : a + b a + c) :
b c
theorem add_le_add_right {α : Type u_1} [has_add α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {b c : α} (bc : b c) (a : α) :
b + a c + a
theorem mul_le_mul_right' {α : Type u_1} [has_mul α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {b c : α} (bc : b c) (a : α) :
b * a c * a
theorem le_of_mul_le_mul_right' {α : Type u_1} [has_mul α] [has_le α] [contravariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} (bc : b * a c * a) :
b c
theorem le_of_add_le_add_right {α : Type u_1} [has_add α] [has_le α] [contravariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} (bc : b + a c + a) :
b c
@[simp]
theorem mul_le_mul_iff_left {α : Type u_1} [has_mul α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [contravariant_class α α has_mul.mul has_le.le] (a : α) {b c : α} :
a * b a * c b c
@[simp]
theorem add_le_add_iff_left {α : Type u_1} [has_add α] [has_le α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_le.le] (a : α) {b c : α} :
a + b a + c b c
@[simp]
theorem mul_le_mul_iff_right {α : Type u_1} [has_mul α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] [contravariant_class α α (function.swap has_mul.mul) has_le.le] (a : α) {b c : α} :
b * a c * a b c
@[simp]
theorem add_le_add_iff_right {α : Type u_1} [has_add α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] [contravariant_class α α (function.swap has_add.add) has_le.le] (a : α) {b c : α} :
b + a c + a b c
@[simp]
theorem mul_lt_mul_iff_left {α : Type u_1} [has_mul α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [contravariant_class α α has_mul.mul has_lt.lt] (a : α) {b c : α} :
a * b < a * c b < c
@[simp]
theorem add_lt_add_iff_left {α : Type u_1} [has_add α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [contravariant_class α α has_add.add has_lt.lt] (a : α) {b c : α} :
a + b < a + c b < c
@[simp]
theorem mul_lt_mul_iff_right {α : Type u_1} [has_mul α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] [contravariant_class α α (function.swap has_mul.mul) has_lt.lt] (a : α) {b c : α} :
b * a < c * a b < c
@[simp]
theorem add_lt_add_iff_right {α : Type u_1} [has_add α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] [contravariant_class α α (function.swap has_add.add) has_lt.lt] (a : α) {b c : α} :
b + a < c + a b < c
theorem add_lt_add_left {α : Type u_1} [has_add α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {b c : α} (bc : b < c) (a : α) :
a + b < a + c
theorem mul_lt_mul_left' {α : Type u_1} [has_mul α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {b c : α} (bc : b < c) (a : α) :
a * b < a * c
theorem lt_of_add_lt_add_left {α : Type u_1} [has_add α] [has_lt α] [contravariant_class α α has_add.add has_lt.lt] {a b c : α} (bc : a + b < a + c) :
b < c
theorem lt_of_mul_lt_mul_left' {α : Type u_1} [has_mul α] [has_lt α] [contravariant_class α α has_mul.mul has_lt.lt] {a b c : α} (bc : a * b < a * c) :
b < c
theorem mul_lt_mul_right' {α : Type u_1} [has_mul α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {b c : α} (bc : b < c) (a : α) :
b * a < c * a
theorem add_lt_add_right {α : Type u_1} [has_add α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {b c : α} (bc : b < c) (a : α) :
b + a < c + a
theorem lt_of_add_lt_add_right {α : Type u_1} [has_add α] [has_lt α] [contravariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} (bc : b + a < c + a) :
b < c
theorem lt_of_mul_lt_mul_right' {α : Type u_1} [has_mul α] [has_lt α] [contravariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c : α} (bc : b * a < c * a) :
b < c
@[simp]
theorem le_add_iff_nonneg_right {α : Type u_1} [add_zero_class α] [has_le α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_le.le] (a : α) {b : α} :
a a + b 0 b
@[simp]
theorem le_mul_iff_one_le_right' {α : Type u_1} [mul_one_class α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [contravariant_class α α has_mul.mul has_le.le] (a : α) {b : α} :
a a * b 1 b
@[simp]
theorem add_le_iff_nonpos_right {α : Type u_1} [add_zero_class α] [has_le α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_le.le] (a : α) {b : α} :
a + b a b 0
@[simp]
theorem mul_le_iff_le_one_right' {α : Type u_1} [mul_one_class α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [contravariant_class α α has_mul.mul has_le.le] (a : α) {b : α} :
a * b a b 1
@[simp]
@[simp]
theorem exists_square_le {α : Type u_1} [mul_one_class α] [linear_order α] [covariant_class α α has_mul.mul has_lt.lt] (a : α) :
∃ (b : α), b * b a
theorem lt_add_of_pos_right {α : Type u_1} [add_zero_class α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] (a : α) {b : α} (h : 0 < b) :
a < a + b
theorem lt_mul_of_one_lt_right' {α : Type u_1} [mul_one_class α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] (a : α) {b : α} (h : 1 < b) :
a < a * b
@[simp]
theorem lt_add_iff_pos_right {α : Type u_1} [add_zero_class α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [contravariant_class α α has_add.add has_lt.lt] (a : α) {b : α} :
a < a + b 0 < b
@[simp]
theorem lt_mul_iff_one_lt_right' {α : Type u_1} [mul_one_class α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [contravariant_class α α has_mul.mul has_lt.lt] (a : α) {b : α} :
a < a * b 1 < b
@[simp]
theorem add_lt_iff_neg_left {α : Type u_1} [add_zero_class α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [contravariant_class α α has_add.add has_lt.lt] {a b : α} :
a + b < a b < 0
@[simp]
theorem mul_lt_iff_lt_one_left' {α : Type u_1} [mul_one_class α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [contravariant_class α α has_mul.mul has_lt.lt] {a b : α} :
a * b < a b < 1
@[simp]
theorem lt_add_iff_pos_left {α : Type u_1} [add_zero_class α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] [contravariant_class α α (function.swap has_add.add) has_lt.lt] (a : α) {b : α} :
a < b + a 0 < b
@[simp]
theorem lt_mul_iff_one_lt_left' {α : Type u_1} [mul_one_class α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] [contravariant_class α α (function.swap has_mul.mul) has_lt.lt] (a : α) {b : α} :
a < b * a 1 < b
@[simp]
theorem add_lt_iff_neg_right {α : Type u_1} [add_zero_class α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] [contravariant_class α α (function.swap has_add.add) has_lt.lt] {a : α} (b : α) :
a + b < b a < 0
@[simp]
theorem mul_lt_iff_lt_one_right' {α : Type u_1} [mul_one_class α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] [contravariant_class α α (function.swap has_mul.mul) has_lt.lt] {a : α} (b : α) :
a * b < b a < 1
theorem mul_le_of_le_of_le_one {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} (hbc : b c) (ha : a 1) :
b * a c
theorem add_le_of_le_of_nonpos {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b c : α} (hbc : b c) (ha : a 0) :
b + a c
theorem mul_le_one' {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} (hbc : b c) (ha : a 1) :
b * a c

Alias of mul_le_of_le_of_le_one.

theorem add_nonpos {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b c : α} (hbc : b c) (ha : a 0) :
b + a c
theorem lt_mul_of_lt_of_one_le {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} (hbc : b < c) (ha : 1 a) :
b < c * a
theorem lt_add_of_lt_of_nonneg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b c : α} (hbc : b < c) (ha : 0 a) :
b < c + a
theorem add_lt_of_lt_of_nonpos {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b c : α} (hbc : b < c) (ha : a 0) :
b + a < c
theorem mul_lt_of_lt_of_le_one {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} (hbc : b < c) (ha : a 1) :
b * a < c
theorem lt_add_of_le_of_pos {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} (hbc : b c) (ha : 0 < a) :
b < c + a
theorem lt_mul_of_le_of_one_lt {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} (hbc : b c) (ha : 1 < a) :
b < c * a
theorem mul_lt_of_le_one_of_lt {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} (ha : a 1) (hb : b < c) :
a * b < c
theorem add_lt_of_nonpos_of_lt {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} (ha : a 0) (hb : b < c) :
a + b < c
theorem add_le_of_nonpos_of_le {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} (ha : a 0) (hbc : b c) :
a + b c
theorem mul_le_of_le_one_of_le {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} (ha : a 1) (hbc : b c) :
a * b c
theorem le_add_of_nonneg_of_le {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} (ha : 0 a) (hbc : b c) :
b a + c
theorem le_mul_of_one_le_of_le {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} (ha : 1 a) (hbc : b c) :
b a * c
theorem left.mul_lt_one {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a b : α} (ha : a < 1) (hb : b < 1) :
a * b < 1

Assume monotonicity on the left. The lemma assuming right is right.mul_lt_one.

theorem left.add_neg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a b : α} (ha : a < 0) (hb : b < 0) :
a + b < 0
theorem right.add_neg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} (ha : a < 0) (hb : b < 0) :
a + b < 0
theorem right.mul_lt_one {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} (ha : a < 1) (hb : b < 1) :
a * b < 1

Assume monotonicity on the right. The lemma assuming left is left.mul_lt_one.

theorem add_lt_of_le_of_neg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} (hbc : b c) (ha : a < 0) :
b + a < c
theorem mul_lt_of_le_of_lt_one {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} (hbc : b c) (ha : a < 1) :
b * a < c
theorem mul_lt_of_lt_one_of_le {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c : α} (ha : a < 1) (hbc : b c) :
a * b < c
theorem add_lt_of_neg_of_le {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} (ha : a < 0) (hbc : b c) :
a + b < c
theorem lt_add_of_pos_of_le {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} (ha : 0 < a) (hbc : b c) :
b < a + c
theorem lt_mul_of_one_lt_of_le {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c : α} (ha : 1 < a) (hbc : b c) :
b < a * c
theorem le_mul_of_le_of_le_one {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} (ha : c a) (hb : 1 b) :
c a * b

Assumes left covariance.

theorem le_add_of_le_of_nonpos {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b c : α} (ha : c a) (hb : 0 b) :
c a + b
theorem one_le_mul {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : 1 a) (hb : 1 b) :
1 a * b
theorem add_nonneg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : 0 a) (hb : 0 b) :
0 a + b
theorem lt_mul_of_lt_of_one_lt {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} (ha : c < a) (hb : 1 < b) :
c < a * b

Assumes left covariance.

theorem lt_add_of_lt_of_pos {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} (ha : c < a) (hb : 0 < b) :
c < a + b
theorem left.mul_lt_one_of_lt_of_lt_one {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} (ha : a < c) (hb : b < 1) :
a * b < c

Assumes left covariance.

theorem left.add_neg_of_lt_of_neg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} (ha : a < c) (hb : b < 0) :
a + b < c
theorem right.mul_lt_one_of_lt_of_lt_one {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c : α} (ha : a < 1) (hb : b < c) :
a * b < c

Assumes right covariance.

theorem right.add_neg_of_lt_of_neg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} (ha : a < 0) (hb : b < c) :
a + b < c
theorem right.add_nonneg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} (ha : 0 a) (hb : 0 b) :
0 a + b
theorem right.one_le_mul {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} (ha : 1 a) (hb : 1 b) :
1 a * b

Assumes right covariance.

theorem right.add_pos {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {b : α} (hb : 0 < b) {a : α} (ha : 0 < a) :
0 < a + b
theorem right.one_lt_mul {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {b : α} (hb : 1 < b) {a : α} (ha : 1 < a) :
1 < a * b

Assumes right covariance.

theorem le_add_of_nonneg_right {α : Type u_1} [add_zero_class α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b : α} (h : 0 b) :
a a + b
theorem le_mul_of_one_le_right' {α : Type u_1} [mul_one_class α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (h : 1 b) :
a a * b
theorem mul_le_of_le_one_right' {α : Type u_1} [mul_one_class α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (h : b 1) :
a * b a
theorem add_le_of_nonpos_right {α : Type u_1} [add_zero_class α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b : α} (h : b 0) :
a + b a
theorem add_left_cancel'' {α : Type u_1} [add_semigroup α] [partial_order α] [contravariant_class α α has_add.add has_le.le] {a b c : α} (h : a + b = a + c) :
b = c
theorem mul_left_cancel'' {α : Type u_1} [semigroup α] [partial_order α] [contravariant_class α α has_mul.mul has_le.le] {a b c : α} (h : a * b = a * c) :
b = c
theorem add_right_cancel'' {α : Type u_1} [add_semigroup α] [partial_order α] [contravariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} (h : a + b = c + b) :
a = c
theorem mul_right_cancel'' {α : Type u_1} [semigroup α] [partial_order α] [contravariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} (h : a * b = c * b) :
a = c

A semigroup with a partial order and satisfying left_cancel_semigroup (i.e. a * c < b * c → a < b) is a left_cancel semigroup.

Equations

An additive semigroup with a partial order and satisfying left_cancel_add_semigroup (i.e. c + a < c + b → a < b) is a left_cancel add_semigroup.

Equations

An additive semigroup with a partial order and satisfying right_cancel_add_semigroup (a + c < b + c → a < b) is a right_cancel add_semigroup.

Equations

A semigroup with a partial order and satisfying right_cancel_semigroup (i.e. a * c < b * c → a < b) is a right_cancel semigroup.

Equations
theorem mul_lt_mul_of_lt_of_lt {α : Type u_1} {a b c d : α} [preorder α] [has_mul α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (h₁ : a < b) (h₂ : c < d) :
a * c < b * d
theorem add_lt_add_of_lt_of_lt {α : Type u_1} {a b c d : α} [preorder α] [has_add α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] (h₁ : a < b) (h₂ : c < d) :
a + c < b + d
theorem mul_lt_mul_of_le_of_lt {α : Type u_1} {a b c d : α} [preorder α] [has_mul α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_le.le] (h₁ : a b) (h₂ : c < d) :
a * c < b * d
theorem add_lt_add_of_le_of_lt {α : Type u_1} {a b c d : α} [preorder α] [has_add α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_le.le] (h₁ : a b) (h₂ : c < d) :
a + c < b + d
theorem mul_lt_mul''' {α : Type u_1} {a b c d : α} [preorder α] [has_mul α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_le.le] (h₁ : a < b) (h₂ : c < d) :
a * c < b * d
theorem add_lt_add {α : Type u_1} {a b c d : α} [preorder α] [has_add α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_le.le] (h₁ : a < b) (h₂ : c < d) :
a + c < b + d
theorem mul_lt_of_mul_lt_left {α : Type u_1} {a b c d : α} [preorder α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] (h : a * b < c) (hle : d b) :
a * d < c
theorem add_lt_of_add_lt_left {α : Type u_1} {a b c d : α} [preorder α] [has_add α] [covariant_class α α has_add.add has_le.le] (h : a + b < c) (hle : d b) :
a + d < c
theorem add_le_of_add_le_left {α : Type u_1} {a b c d : α} [preorder α] [has_add α] [covariant_class α α has_add.add has_le.le] (h : a + b c) (hle : d b) :
a + d c
theorem mul_le_of_mul_le_left {α : Type u_1} {a b c d : α} [preorder α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] (h : a * b c) (hle : d b) :
a * d c
theorem lt_add_of_lt_add_left {α : Type u_1} {a b c d : α} [preorder α] [has_add α] [covariant_class α α has_add.add has_le.le] (h : a < b + c) (hle : c d) :
a < b + d
theorem lt_mul_of_lt_mul_left {α : Type u_1} {a b c d : α} [preorder α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] (h : a < b * c) (hle : c d) :
a < b * d
theorem le_add_of_le_add_left {α : Type u_1} {a b c d : α} [preorder α] [has_add α] [covariant_class α α has_add.add has_le.le] (h : a b + c) (hle : c d) :
a b + d
theorem le_mul_of_le_mul_left {α : Type u_1} {a b c d : α} [preorder α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] (h : a b * c) (hle : c d) :
a b * d
theorem add_lt_add_of_lt_of_le {α : Type u_1} {a b c d : α} [preorder α] [has_add α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_lt.lt] (h₁ : a < b) (h₂ : c d) :
a + c < b + d
theorem mul_lt_mul_of_lt_of_le {α : Type u_1} {a b c d : α} [preorder α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (h₁ : a < b) (h₂ : c d) :
a * c < b * d

Here we start using properties of one, on the left.

theorem lt_of_mul_lt_of_one_le_left {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] (h : a * b < c) (hle : 1 b) :
a < c
theorem lt_of_add_lt_of_nonneg_left {α : Type u_1} {a b c : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] (h : a + b < c) (hle : 0 b) :
a < c
theorem le_of_mul_le_of_one_le_left {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] (h : a * b c) (hle : 1 b) :
a c
theorem le_of_add_le_of_nonneg_left {α : Type u_1} {a b c : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] (h : a + b c) (hle : 0 b) :
a c
theorem lt_of_lt_add_of_nonpos_left {α : Type u_1} {a b c : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] (h : a < b + c) (hle : c 0) :
a < b
theorem lt_of_lt_mul_of_le_one_left {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] (h : a < b * c) (hle : c 1) :
a < b
theorem le_of_le_add_of_nonpos_left {α : Type u_1} {a b c : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] (h : a b + c) (hle : c 0) :
a b
theorem le_of_le_mul_of_le_one_left {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] (h : a b * c) (hle : c 1) :
a b
theorem mul_lt_of_lt_of_lt_one {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] (bc : b < c) (a1 : a < 1) :
b * a < c
theorem add_lt_of_lt_of_neg {α : Type u_1} {a b c : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] (bc : b < c) (a1 : a < 0) :
b + a < c
theorem mul_lt_of_mul_lt_right {α : Type u_1} {a b c d : α} [preorder α] [has_mul α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (h : a * b < c) (hle : d a) :
d * b < c
theorem add_lt_of_add_lt_right {α : Type u_1} {a b c d : α} [preorder α] [has_add α] [covariant_class α α (function.swap has_add.add) has_le.le] (h : a + b < c) (hle : d a) :
d + b < c
theorem mul_le_of_mul_le_right {α : Type u_1} {a b c d : α} [preorder α] [has_mul α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (h : a * b c) (hle : d a) :
d * b c
theorem add_le_of_add_le_right {α : Type u_1} {a b c d : α} [preorder α] [has_add α] [covariant_class α α (function.swap has_add.add) has_le.le] (h : a + b c) (hle : d a) :
d + b c
theorem lt_add_of_lt_add_right {α : Type u_1} {a b c d : α} [preorder α] [has_add α] [covariant_class α α (function.swap has_add.add) has_le.le] (h : a < b + c) (hle : b d) :
a < d + c
theorem lt_mul_of_lt_mul_right {α : Type u_1} {a b c d : α} [preorder α] [has_mul α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (h : a < b * c) (hle : b d) :
a < d * c
theorem le_mul_of_le_mul_right {α : Type u_1} {a b c d : α} [preorder α] [has_mul α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (h : a b * c) (hle : b d) :
a d * c
theorem le_add_of_le_add_right {α : Type u_1} {a b c d : α} [preorder α] [has_add α] [covariant_class α α (function.swap has_add.add) has_le.le] (h : a b + c) (hle : b d) :
a d + c
theorem add_le_add {α : Type u_1} {a b c d : α} [preorder α] [has_add α] [covariant_class α α (function.swap has_add.add) has_le.le] [covariant_class α α has_add.add has_le.le] (h₁ : a b) (h₂ : c d) :
a + c b + d
theorem mul_le_mul' {α : Type u_1} {a b c d : α} [preorder α] [has_mul α] [covariant_class α α (function.swap has_mul.mul) has_le.le] [covariant_class α α has_mul.mul has_le.le] (h₁ : a b) (h₂ : c d) :
a * c b * d
theorem mul_le_mul_three {α : Type u_1} {a b c d : α} [preorder α] [has_mul α] [covariant_class α α (function.swap has_mul.mul) has_le.le] [covariant_class α α has_mul.mul has_le.le] {e f : α} (h₁ : a d) (h₂ : b e) (h₃ : c f) :
(a * b) * c (d * e) * f
theorem add_le_add_three {α : Type u_1} {a b c d : α} [preorder α] [has_add α] [covariant_class α α (function.swap has_add.add) has_le.le] [covariant_class α α has_add.add has_le.le] {e f : α} (h₁ : a d) (h₂ : b e) (h₃ : c f) :
a + b + c d + e + f

Here we start using properties of one, on the right.

theorem le_mul_of_one_le_left' {α : Type u_1} {a b : α} [preorder α] [mul_one_class α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (h : 1 b) :
a b * a
theorem le_add_of_nonneg_left {α : Type u_1} {a b : α} [preorder α] [add_zero_class α] [covariant_class α α (function.swap has_add.add) has_le.le] (h : 0 b) :
a b + a
theorem add_le_of_nonpos_left {α : Type u_1} {a b : α} [preorder α] [add_zero_class α] [covariant_class α α (function.swap has_add.add) has_le.le] (h : b 0) :
b + a a
theorem mul_le_of_le_one_left' {α : Type u_1} {a b : α} [preorder α] [mul_one_class α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (h : b 1) :
b * a a
theorem lt_of_mul_lt_of_one_le_right {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (h : a * b < c) (hle : 1 a) :
b < c
theorem lt_of_add_lt_of_nonneg_right {α : Type u_1} {a b c : α} [preorder α] [add_zero_class α] [covariant_class α α (function.swap has_add.add) has_le.le] (h : a + b < c) (hle : 0 a) :
b < c
theorem le_of_mul_le_of_one_le_right {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (h : a * b c) (hle : 1 a) :
b c
theorem le_of_add_le_of_nonneg_right {α : Type u_1} {a b c : α} [preorder α] [add_zero_class α] [covariant_class α α (function.swap has_add.add) has_le.le] (h : a + b c) (hle : 0 a) :
b c
theorem lt_of_lt_add_of_nonpos_right {α : Type u_1} {a b c : α} [preorder α] [add_zero_class α] [covariant_class α α (function.swap has_add.add) has_le.le] (h : a < b + c) (hle : b 0) :
a < c
theorem lt_of_lt_mul_of_le_one_right {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (h : a < b * c) (hle : b 1) :
a < c
theorem le_of_le_mul_of_le_one_right {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (h : a b * c) (hle : b 1) :
a c
theorem le_of_le_add_of_nonpos_right {α : Type u_1} {a b c : α} [preorder α] [add_zero_class α] [covariant_class α α (function.swap has_add.add) has_le.le] (h : a b + c) (hle : b 0) :
a c
theorem mul_lt_of_lt_one_of_lt {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a1 : a < 1) (bc : b < c) :
a * b < c
theorem lt_add_of_pos_left {α : Type u_1} [preorder α] [add_zero_class α] [covariant_class α α (function.swap has_add.add) has_lt.lt] (a : α) {b : α} (h : 0 < b) :
a < b + a
theorem lt_mul_of_one_lt_left' {α : Type u_1} [preorder α] [mul_one_class α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (a : α) {b : α} (h : 1 < b) :
a < b * a
theorem one_lt_mul_of_lt_of_le' {α : Type u_1} {a b : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] (ha : 1 < a) (hb : 1 b) :
1 < a * b
theorem add_pos_of_pos_of_nonneg {α : Type u_1} {a b : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] (ha : 0 < a) (hb : 0 b) :
0 < a + b
theorem one_lt_mul' {α : Type u_1} {a b : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] (ha : 1 < a) (hb : 1 < b) :
1 < a * b
theorem add_pos {α : Type u_1} {a b : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] (ha : 0 < a) (hb : 0 < b) :
0 < a + b
theorem lt_mul_of_lt_of_one_le' {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] (hbc : b < c) (ha : 1 a) :
b < c * a
theorem lt_add_of_lt_of_nonneg' {α : Type u_1} {a b c : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] (hbc : b < c) (ha : 0 a) :
b < c + a
theorem lt_add_of_lt_of_pos' {α : Type u_1} {a b c : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] (hbc : b < c) (ha : 0 < a) :
b < c + a
theorem lt_mul_of_lt_of_one_lt' {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] (hbc : b < c) (ha : 1 < a) :
b < c * a
theorem le_add_of_le_of_nonneg {α : Type u_1} {a b c : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] (hbc : b c) (ha : 0 a) :
b c + a
theorem le_mul_of_le_of_one_le {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] (hbc : b c) (ha : 1 a) :
b c * a
theorem one_le_mul_right {α : Type u_1} {a b : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] (ha : 1 a) (hb : 1 b) :
1 a * b
theorem add_pos_of_nonneg_of_pos {α : Type u_1} {a b : α} [preorder α] [add_zero_class α] [covariant_class α α (function.swap has_add.add) has_le.le] (ha : 0 a) (hb : 0 < b) :
0 < a + b
theorem one_lt_mul_of_le_of_lt' {α : Type u_1} {a b : α} [preorder α] [mul_one_class α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ha : 1 a) (hb : 1 < b) :
1 < a * b
theorem lt_mul_of_one_le_of_lt {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ha : 1 a) (hbc : b < c) :
b < a * c
theorem lt_add_of_nonneg_of_lt {α : Type u_1} {a b c : α} [preorder α] [add_zero_class α] [covariant_class α α (function.swap has_add.add) has_le.le] (ha : 0 a) (hbc : b < c) :
b < a + c
theorem lt_mul_of_one_lt_of_lt {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ha : 1 < a) (hbc : b < c) :
b < a * c
theorem lt_add_of_pos_of_lt {α : Type u_1} {a b c : α} [preorder α] [add_zero_class α] [covariant_class α α (function.swap has_add.add) has_le.le] (ha : 0 < a) (hbc : b < c) :
b < a + c

Properties assuming partial_order.

theorem add_eq_zero_iff' {α : Type u_1} {a b : α} [add_zero_class α] [partial_order α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (ha : 0 a) (hb : 0 b) :
a + b = 0 a = 0 b = 0
theorem mul_eq_one_iff' {α : Type u_1} {a b : α} [mul_one_class α] [partial_order α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ha : 1 a) (hb : 1 b) :
a * b = 1 a = 1 b = 1
theorem monotone.const_add {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f : β → α} [covariant_class α α has_add.add has_le.le] (hf : monotone f) (a : α) :
monotone (λ (x : β), a + f x)
theorem monotone.const_mul' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f : β → α} [covariant_class α α has_mul.mul has_le.le] (hf : monotone f) (a : α) :
monotone (λ (x : β), a * f x)
theorem monotone.add_const {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f : β → α} [covariant_class α α (function.swap has_add.add) has_le.le] (hf : monotone f) (a : α) :
monotone (λ (x : β), f x + a)
theorem monotone.mul_const' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f : β → α} [covariant_class α α (function.swap has_mul.mul) has_le.le] (hf : monotone f) (a : α) :
monotone (λ (x : β), (f x) * a)
theorem monotone.mul' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f g : β → α} [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (hf : monotone f) (hg : monotone g) :
monotone (λ (x : β), (f x) * g x)

The product of two monotone functions is monotone.

theorem monotone.add {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f g : β → α} [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (hf : monotone f) (hg : monotone g) :
monotone (λ (x : β), f x + g x)

The sum of two monotone functions is monotone.

theorem strict_mono.const_add {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f : β → α} [covariant_class α α has_add.add has_lt.lt] (hf : strict_mono f) (c : α) :
strict_mono (λ (x : β), c + f x)
theorem strict_mono.const_mul' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f : β → α} [covariant_class α α has_mul.mul has_lt.lt] (hf : strict_mono f) (c : α) :
strict_mono (λ (x : β), c * f x)
theorem strict_mono.add_const {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f : β → α} [covariant_class α α (function.swap has_add.add) has_lt.lt] (hf : strict_mono f) (c : α) :
strict_mono (λ (x : β), f x + c)
theorem strict_mono.mul_const' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f : β → α} [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (hf : strict_mono f) (c : α) :
strict_mono (λ (x : β), (f x) * c)
theorem strict_mono.mul' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f g : β → α} [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (hf : strict_mono f) (hg : strict_mono g) :
strict_mono (λ (x : β), (f x) * g x)

The product of two strictly monotone functions is strictly monotone.

theorem strict_mono.add {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f g : β → α} [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] (hf : strict_mono f) (hg : strict_mono g) :
strict_mono (λ (x : β), f x + g x)

The sum of two strictly monotone functions is strictly monotone.

theorem monotone.mul_strict_mono' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_le.le] {f g : β → α} (hf : monotone f) (hg : strict_mono g) :
strict_mono (λ (x : β), (f x) * g x)

The product of a monotone function and a strictly monotone function is strictly monotone.

theorem monotone.add_strict_mono {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_le.le] {f g : β → α} (hf : monotone f) (hg : strict_mono g) :
strict_mono (λ (x : β), f x + g x)

The sum of a monotone function and a strictly monotone function is strictly monotone.

theorem strict_mono.add_monotone {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f g : β → α} [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_lt.lt] (hf : strict_mono f) (hg : monotone g) :
strict_mono (λ (x : β), f x + g x)

The sum of a strictly monotone function and a monotone function is strictly monotone.

theorem strict_mono.mul_monotone' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f g : β → α} [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (hf : strict_mono f) (hg : monotone g) :
strict_mono (λ (x : β), (f x) * g x)

The product of a strictly monotone function and a monotone function is strictly monotone.

def add_le_cancellable {α : Type u_1} [has_add α] [has_le α] (a : α) :
Prop

An element a : α is add_le_cancellable if x ↦ a + x is order-reflecting. We will make a separate version of many lemmas that require [contravariant_class α α (+) (≤)] with mul_le_cancellable assumptions instead. These lemmas can then be instantiated to specific types, like ennreal, where we can replace the assumption add_le_cancellable x by x ≠ ∞.

Equations
def mul_le_cancellable {α : Type u_1} [has_mul α] [has_le α] (a : α) :
Prop

An element a : α is mul_le_cancellable if x ↦ a * x is order-reflecting. We will make a separate version of many lemmas that require [contravariant_class α α (*) (≤)] with mul_le_cancellable assumptions instead. These lemmas can then be instantiated to specific types, like ennreal, where we can replace the assumption add_le_cancellable x by x ≠ ∞.

Equations
theorem mul_le_cancellable.inj {α : Type u_1} [has_mul α] [partial_order α] {a b c : α} (ha : mul_le_cancellable a) :
a * b = a * c b = c
theorem add_le_cancellable.inj {α : Type u_1} [has_add α] [partial_order α] {a b c : α} (ha : add_le_cancellable a) :
a + b = a + c b = c
theorem add_le_cancellable.injective_left {α : Type u_1} [add_comm_semigroup α] [partial_order α] {a : α} (ha : add_le_cancellable a) :
function.injective (λ (_x : α), _x + a)
theorem mul_le_cancellable.injective_left {α : Type u_1} [comm_semigroup α] [partial_order α] {a : α} (ha : mul_le_cancellable a) :
function.injective (λ (_x : α), _x * a)
theorem add_le_cancellable.inj_left {α : Type u_1} [add_comm_semigroup α] [partial_order α] {a b c : α} (hc : add_le_cancellable c) :
a + c = b + c a = b
theorem mul_le_cancellable.inj_left {α : Type u_1} [comm_semigroup α] [partial_order α] {a b c : α} (hc : mul_le_cancellable c) :
a * c = b * c a = b
theorem mul_le_cancellable.mul_le_mul_iff_left {α : Type u_1} [has_le α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} (ha : mul_le_cancellable a) :
a * b a * c b c
theorem add_le_cancellable.add_le_add_iff_left {α : Type u_1} [has_le α] [has_add α] [covariant_class α α has_add.add has_le.le] {a b c : α} (ha : add_le_cancellable a) :
a + b a + c b c
theorem mul_le_cancellable.mul_le_mul_iff_right {α : Type u_1} [has_le α] [comm_semigroup α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} (ha : mul_le_cancellable a) :
b * a c * a b c
theorem add_le_cancellable.add_le_add_iff_right {α : Type u_1} [has_le α] [add_comm_semigroup α] [covariant_class α α has_add.add has_le.le] {a b c : α} (ha : add_le_cancellable a) :
b + a c + a b c
theorem add_le_cancellable.le_add_iff_nonneg_right {α : Type u_1} [has_le α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : add_le_cancellable a) :
a a + b 0 b
theorem mul_le_cancellable.le_mul_iff_one_le_right {α : Type u_1} [has_le α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : mul_le_cancellable a) :
a a * b 1 b
theorem mul_le_cancellable.mul_le_iff_le_one_right {α : Type u_1} [has_le α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : mul_le_cancellable a) :
a * b a b 1
theorem add_le_cancellable.add_le_iff_nonpos_right {α : Type u_1} [has_le α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : add_le_cancellable a) :
a + b a b 0
theorem add_le_cancellable.le_add_iff_nonneg_left {α : Type u_1} [has_le α] [add_comm_monoid α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : add_le_cancellable a) :
a b + a 0 b
theorem mul_le_cancellable.le_mul_iff_one_le_left {α : Type u_1} [has_le α] [comm_monoid α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : mul_le_cancellable a) :
a b * a 1 b
theorem add_le_cancellable.add_le_iff_nonpos_left {α : Type u_1} [has_le α] [add_comm_monoid α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : add_le_cancellable a) :
b + a a b 0
theorem mul_le_cancellable.mul_le_iff_le_one_left {α : Type u_1} [has_le α] [comm_monoid α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : mul_le_cancellable a) :
b * a a b 1