• exists_mul_of_le : ∀ {a b : α}, a ≤ b → (∃ (c : α), b = a * c)

An ordered_comm_monoid with one-sided 'division' in the sense that if a ≤ b, there is some c for which a * c = b. This is a weaker version of the condition on canonical orderings defined by canonically_ordered_monoid.

• exists_add_of_le : ∀ {a b : α}, a ≤ b → (∃ (c : α), b = a + c)

An ordered_add_comm_monoid with one-sided 'subtraction' in the sense that if a ≤ b, then there is some c for which a + c = b. This is a weaker version of the condition on canonical orderings defined by canonically_ordered_add_monoid.

• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero' : (∀ (x : α), canonically_ordered_add_monoid.nsmul 0 x = 0) . "try_refl_tac"
• nsmul_succ' : (∀ (n : ℕ) (x : α), canonically_ordered_add_monoid.nsmul n.succ x = x + canonically_ordered_add_monoid.nsmul n x) . "try_refl_tac"
• add_comm : ∀ (a b : α), a + b = b + a
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
• bot : α
• bot_le : ∀ (x : α), ⊥ ≤ x
• exists_add_of_le : ∀ {a b : α}, a ≤ b → (∃ (c : α), b = a + c)
• le_self_add : ∀ (a b : α), a ≤ a + b

A canonically ordered additive monoid is an ordered commutative additive monoid in which the ordering coincides with the subtractibility relation, which is to say, a ≤ b iff there exists c with b = a + c. This is satisfied by the natural numbers, for example, but not the integers or other nontrivial ordered_add_comm_groups.

• mul : α → α → α
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : ℕ → α → α
• npow_zero' : (∀ (x : α), canonically_ordered_monoid.npow 0 x = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ℕ) (x : α), canonically_ordered_monoid.npow n.succ x = x * canonically_ordered_monoid.npow n x) . "try_refl_tac"
• mul_comm : ∀ (a b : α), a * b = b * a
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b
• bot : α
• bot_le : ∀ (x : α), ⊥ ≤ x
• exists_mul_of_le : ∀ {a b : α}, a ≤ b → (∃ (c : α), b = a * c)
• le_self_mul : ∀ (a b : α), a ≤ a * b

A canonically ordered monoid is an ordered commutative monoid in which the ordering coincides with the divisibility relation, which is to say, a ≤ b iff there exists c with b = a * c. Examples seem rare; it seems more likely that the order_dual of a naturally-occurring lattice satisfies this than the lattice itself (for example, dual of the lattice of ideals of a PID or Dedekind domain satisfy this; collections of all things ≤ 1 seem to be more natural that collections of all things ≥ 1).

• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero' : (∀ (x : α), canonically_linear_ordered_add_monoid.nsmul 0 x = 0) . "try_refl_tac"
• nsmul_succ' : (∀ (n : ℕ) (x : α), canonically_linear_ordered_add_monoid.nsmul n.succ x = x + canonically_linear_ordered_add_monoid.nsmul n x) . "try_refl_tac"
• add_comm : ∀ (a b : α), a + b = b + a
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
• bot : α
• bot_le : ∀ (x : α), ⊥ ≤ x
• exists_add_of_le : ∀ {a b : α}, a ≤ b → (∃ (c : α), b = a + c)
• le_self_add : ∀ (a b : α), a ≤ a + b
• le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
• decidable_le : decidable_rel has_le.le
• decidable_eq : decidable_eq α
• decidable_lt : decidable_rel has_lt.lt
• max : α → α → α
• max_def : canonically_linear_ordered_add_monoid.max = max_default . "reflexivity"
• min : α → α → α
• min_def : canonically_linear_ordered_add_monoid.min = min_default . "reflexivity"

A canonically linear-ordered additive monoid is a canonically ordered additive monoid whose ordering is a linear order.

• mul : α → α → α
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : ℕ → α → α
• npow_zero' : (∀ (x : α), canonically_linear_ordered_monoid.npow 0 x = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ℕ) (x : α), canonically_linear_ordered_monoid.npow n.succ x = x * canonically_linear_ordered_monoid.npow n x) . "try_refl_tac"
• mul_comm : ∀ (a b : α), a * b = b * a
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b
• bot : α
• bot_le : ∀ (x : α), ⊥ ≤ x
• exists_mul_of_le : ∀ {a b : α}, a ≤ b → (∃ (c : α), b = a * c)
• le_self_mul : ∀ (a b : α), a ≤ a * b
• le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
• decidable_le : decidable_rel has_le.le
• decidable_eq : decidable_eq α
• decidable_lt : decidable_rel has_lt.lt
• max : α → α → α
• max_def : canonically_linear_ordered_monoid.max = max_default . "reflexivity"
• min : α → α → α
• min_def : canonically_linear_ordered_monoid.min = min_default . "reflexivity"

A canonically linear-ordered monoid is a canonically ordered monoid whose ordering is a linear order.