diff --git a/src/algebra/group/defs.lean b/src/algebra/group/defs.lean index 0515b58bf2407..7661e5c55259a 100644 --- a/src/algebra/group/defs.lean +++ b/src/algebra/group/defs.lean @@ -207,13 +207,19 @@ class comm_monoid (M : Type u) extends monoid M, comm_semigroup M class add_comm_monoid (M : Type u) extends add_monoid M, add_comm_semigroup M attribute [to_additive add_comm_monoid] comm_monoid +/-- A monoid in which multiplication is left-cancellative. -/ +@[protect_proj, ancestor left_cancel_semigroup monoid] +class left_cancel_monoid (M : Type u) extends left_cancel_semigroup M, monoid M + /-- An additive monoid in which addition is left-cancellative. Main examples are `ℕ` and groups. This is the right typeclass for many sum lemmas, as having a zero is useful to define the sum over the empty set, so `add_left_cancel_semigroup` is not enough. -/ -@[protect_proj] +@[protect_proj, ancestor add_left_cancel_semigroup add_monoid] class add_left_cancel_monoid (M : Type u) extends add_left_cancel_semigroup M, add_monoid M -- TODO: I found 1 (one) lemma assuming `[add_left_cancel_monoid]`. --- Should we port more lemmas to this typeclass? Should we add a multiplicative version? +-- Should we port more lemmas to this typeclass? + +attribute [to_additive add_left_cancel_monoid] left_cancel_monoid /-- A `group` is a `monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`. -/ @[protect_proj, ancestor monoid has_inv] diff --git a/src/algebra/group/to_additive.lean b/src/algebra/group/to_additive.lean index 8c9c500a69375..af576f97c2f32 100644 --- a/src/algebra/group/to_additive.lean +++ b/src/algebra/group/to_additive.lean @@ -107,17 +107,25 @@ do let n := src.mk_string "_to_additive", @[derive has_reflect, derive inhabited] structure value_type := (tgt : name) (doc : option string) -/-- Dictionary of words used by `to_additive.guess_name` to autogenerate -names. -/ -meta def tokens_dict : native.rb_map string string := -native.rb_map.of_list $ -[("mul", "add"), ("one", "zero"), ("inv", "neg"), ("prod", "sum")] +/-- Dictionary used by `to_additive.guess_name` to autogenerate names. -/ +meta def tr : list string → list string +| ("one" :: "le" :: s) := "nonneg" :: tr s +| ("one" :: "lt" :: s) := "pos" :: tr s +| ("le" :: "one" :: s) := "nonpos" :: tr s +| ("lt" :: "one" :: s) := "neg" :: tr s +| ("mul" :: s) := "add" :: tr s +| ("inv" :: s) := "neg" :: tr s +| ("div" :: s) := "sub" :: tr s +| ("one" :: s) := "zero" :: tr s +| ("prod" :: s) := "sum" :: tr s +| (x :: s) := (x :: tr s) +| [] := [] /-- Autogenerate target name for `to_additive`. -/ meta def guess_name : string → string := -string.map_tokens '_' $ string.map_tokens ''' $ -λ s, (tokens_dict.find s).get_or_else s +λ s, string.intercalate (string.singleton '_') $ +tr (s.split_on '_') meta def target_name (src tgt : name) (dict : name_map name) : tactic name := (if tgt.get_prefix ≠ name.anonymous -- `tgt` is a full name diff --git a/src/algebra/ordered_group.lean b/src/algebra/ordered_group.lean index 5643a0d6d606c..4db2dc79c24a1 100644 --- a/src/algebra/ordered_group.lean +++ b/src/algebra/ordered_group.lean @@ -13,161 +13,223 @@ set_option default_priority 100 -- see Note [default priority] /-! # Ordered monoids and groups + +This file develops the basics of ordered monoids and groups. + +## 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. + -/ universe u variable {α : Type u} +/-- An ordered commutative monoid is a commutative monoid +with a partial order such that + * `a ≤ b → c * a ≤ c * b` (multiplication is monotone) + * `a * b < a * c → b < c`. +-/ +@[protect_proj, ancestor comm_monoid partial_order] +class ordered_comm_monoid (α : Type*) extends comm_monoid α, partial_order α := +(mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b) +(lt_of_mul_lt_mul_left : ∀ a b c : α, a * b < a * c → b < c) + /-- An ordered (additive) commutative monoid is a commutative monoid - with a partial order such that addition is an order embedding, i.e. - `a + b ≤ a + c ↔ b ≤ c`. These monoids are automatically cancellative. -/ -@[protect_proj] + with a partial order such that + * `a ≤ b → c + a ≤ c + b` (addition is monotone) + * `a + b < a + c → b < c`. +-/ +@[protect_proj, ancestor add_comm_monoid partial_order] class ordered_add_comm_monoid (α : Type*) extends add_comm_monoid α, partial_order α := (add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b) (lt_of_add_lt_add_left : ∀ a b c : α, a + b < a + c → b < c) -section ordered_add_comm_monoid -variables [ordered_add_comm_monoid α] {a b c d : α} +attribute [to_additive ordered_add_comm_monoid] ordered_comm_monoid + +section ordered_comm_monoid +variables [ordered_comm_monoid α] {a b c d : α} -lemma add_le_add_left' (h : a ≤ b) : c + a ≤ c + b := -ordered_add_comm_monoid.add_le_add_left a b h c +@[to_additive] +lemma mul_le_mul_left' (h : a ≤ b) : c * a ≤ c * b := +ordered_comm_monoid.mul_le_mul_left a b h c -lemma add_le_add_right' (h : a ≤ b) : a + c ≤ b + c := -add_comm c a ▸ add_comm c b ▸ add_le_add_left' h +@[to_additive] +lemma mul_le_mul_right' (h : a ≤ b) : a * c ≤ b * c := +mul_comm c a ▸ mul_comm c b ▸ mul_le_mul_left' h -lemma lt_of_add_lt_add_left' : a + b < a + c → b < c := -ordered_add_comm_monoid.lt_of_add_lt_add_left a b c +@[to_additive] +lemma lt_of_mul_lt_mul_left' : a * b < a * c → b < c := +ordered_comm_monoid.lt_of_mul_lt_mul_left a b c -lemma add_le_add' (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d := -le_trans (add_le_add_right' h₁) (add_le_add_left' h₂) +@[to_additive] +lemma mul_le_mul' (h₁ : a ≤ b) (h₂ : c ≤ d) : a * c ≤ b * d := +le_trans (mul_le_mul_right' h₁) (mul_le_mul_left' h₂) -lemma le_add_of_nonneg_right' (h : 0 ≤ b) : a ≤ a + b := -have a + 0 ≤ a + b, from add_le_add_left' h, -by rwa add_zero at this +@[to_additive le_add_of_nonneg_right'] +lemma le_mul_of_one_le_right'' (h : 1 ≤ b) : a ≤ a * b := +have a * 1 ≤ a * b, from mul_le_mul_left' h, +by rwa mul_one at this -lemma le_add_of_nonneg_left' (h : 0 ≤ b) : a ≤ b + a := -have 0 + a ≤ b + a, from add_le_add_right' h, -by rwa zero_add at this +@[to_additive le_add_of_nonneg_left'] +lemma le_mul_of_one_le_left'' (h : 1 ≤ b) : a ≤ b * a := +have 1 * a ≤ b * a, from mul_le_mul_right' h, +by rwa one_mul at this -lemma lt_of_add_lt_add_right' (h : a + b < c + b) : a < c := -lt_of_add_lt_add_left' - (show b + a < b + c, begin rw [add_comm b a, add_comm b c], assumption end) +@[to_additive] +lemma lt_of_mul_lt_mul_right' (h : a * b < c * b) : a < c := +lt_of_mul_lt_mul_left' + (show b * a < b * c, begin rw [mul_comm b a, mul_comm b c], assumption end) --- here we start using properties of zero. -lemma le_add_of_nonneg_of_le' (ha : 0 ≤ a) (hbc : b ≤ c) : b ≤ a + c := -zero_add b ▸ add_le_add' ha hbc +-- here we start using properties of one. +@[to_additive] +lemma le_mul_of_one_le_of_le' (ha : 1 ≤ a) (hbc : b ≤ c) : b ≤ a * c := +one_mul b ▸ mul_le_mul' ha hbc -lemma le_add_of_le_of_nonneg' (hbc : b ≤ c) (ha : 0 ≤ a) : b ≤ c + a := -add_zero b ▸ add_le_add' hbc ha +@[to_additive] +lemma le_mul_of_le_of_one_le' (hbc : b ≤ c) (ha : 1 ≤ a) : b ≤ c * a := +mul_one b ▸ mul_le_mul' hbc ha -lemma add_nonneg' (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a + b := -le_add_of_nonneg_of_le' ha hb +@[to_additive add_nonneg'] +lemma one_le_mul' (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ a * b := +le_mul_of_one_le_of_le' ha hb -lemma add_pos_of_pos_of_nonneg' (ha : 0 < a) (hb : 0 ≤ b) : 0 < a + b := -lt_of_lt_of_le ha $ le_add_of_nonneg_right' hb +@[to_additive] +lemma mul_one_lt_of_one_lt_of_one_le' (ha : 1 < a) (hb : 1 ≤ b) : 1 < a * b := +lt_of_lt_of_le ha $ le_mul_of_one_le_right'' hb -lemma add_pos' (ha : 0 < a) (hb : 0 < b) : 0 < a + b := -add_pos_of_pos_of_nonneg' ha $ le_of_lt hb +@[to_additive] +lemma mul_one_lt' (ha : 1 < a) (hb : 1 < b) : 1 < a * b := +mul_one_lt_of_one_lt_of_one_le' ha $ le_of_lt hb -lemma add_pos_of_nonneg_of_pos' (ha : 0 ≤ a) (hb : 0 < b) : 0 < a + b := -lt_of_lt_of_le hb $ le_add_of_nonneg_left' ha +@[to_additive] +lemma mul_one_lt_of_one_le_of_one_lt' (ha : 1 ≤ a) (hb : 1 < b) : 1 < a * b := +lt_of_lt_of_le hb $ le_mul_of_one_le_left'' ha -lemma add_nonpos' (ha : a ≤ 0) (hb : b ≤ 0) : a + b ≤ 0 := -zero_add (0:α) ▸ (add_le_add' ha hb) +@[to_additive] +lemma mul_le_one' (ha : a ≤ 1) (hb : b ≤ 1) : a * b ≤ 1 := +one_mul (1:α) ▸ (mul_le_mul' ha hb) -lemma add_le_of_nonpos_of_le' (ha : a ≤ 0) (hbc : b ≤ c) : a + b ≤ c := -zero_add c ▸ add_le_add' ha hbc +@[to_additive] +lemma mul_le_of_le_one_of_le' (ha : a ≤ 1) (hbc : b ≤ c) : a * b ≤ c := +one_mul c ▸ mul_le_mul' ha hbc -lemma add_le_of_le_of_nonpos' (hbc : b ≤ c) (ha : a ≤ 0) : b + a ≤ c := -add_zero c ▸ add_le_add' hbc ha +@[to_additive] +lemma mul_le_of_le_of_le_one' (hbc : b ≤ c) (ha : a ≤ 1) : b * a ≤ c := +mul_one c ▸ mul_le_mul' hbc ha -lemma add_neg_of_neg_of_nonpos' (ha : a < 0) (hb : b ≤ 0) : a + b < 0 := -lt_of_le_of_lt (add_le_of_le_of_nonpos' (le_refl _) hb) ha +@[to_additive] +lemma mul_lt_one_of_lt_one_of_le_one' (ha : a < 1) (hb : b ≤ 1) : a * b < 1 := +lt_of_le_of_lt (mul_le_of_le_of_le_one' (le_refl _) hb) ha -lemma add_neg_of_nonpos_of_neg' (ha : a ≤ 0) (hb : b < 0) : a + b < 0 := -lt_of_le_of_lt (add_le_of_nonpos_of_le' ha (le_refl _)) hb +@[to_additive] +lemma mul_lt_one_of_le_one_of_lt_one' (ha : a ≤ 1) (hb : b < 1) : a * b < 1 := +lt_of_le_of_lt (mul_le_of_le_one_of_le' ha (le_refl _)) hb -lemma add_neg' (ha : a < 0) (hb : b < 0) : a + b < 0 := -add_neg_of_nonpos_of_neg' (le_of_lt ha) hb +@[to_additive] +lemma mul_lt_one' (ha : a < 1) (hb : b < 1) : a * b < 1 := +mul_lt_one_of_le_one_of_lt_one' (le_of_lt ha) hb -lemma lt_add_of_nonneg_of_lt' (ha : 0 ≤ a) (hbc : b < c) : b < a + c := -lt_of_lt_of_le hbc $ le_add_of_nonneg_left' ha +@[to_additive] +lemma lt_mul_of_one_le_of_lt' (ha : 1 ≤ a) (hbc : b < c) : b < a * c := +lt_of_lt_of_le hbc $ le_mul_of_one_le_left'' ha -lemma lt_add_of_lt_of_nonneg' (hbc : b < c) (ha : 0 ≤ a) : b < c + a := -lt_of_lt_of_le hbc $ le_add_of_nonneg_right' ha +@[to_additive] +lemma lt_mul_of_lt_of_one_le' (hbc : b < c) (ha : 1 ≤ a) : b < c * a := +lt_of_lt_of_le hbc $ le_mul_of_one_le_right'' ha -lemma lt_add_of_pos_of_lt' (ha : 0 < a) (hbc : b < c) : b < a + c := -lt_add_of_nonneg_of_lt' (le_of_lt ha) hbc +@[to_additive] +lemma lt_mul_of_one_lt_of_lt' (ha : 1 < a) (hbc : b < c) : b < a * c := +lt_mul_of_one_le_of_lt' (le_of_lt ha) hbc -lemma lt_add_of_lt_of_pos' (hbc : b < c) (ha : 0 < a) : b < c + a := -lt_add_of_lt_of_nonneg' hbc (le_of_lt ha) +@[to_additive] +lemma lt_mul_of_lt_of_one_lt' (hbc : b < c) (ha : 1 < a) : b < c * a := +lt_mul_of_lt_of_one_le' hbc (le_of_lt ha) -lemma add_lt_of_nonpos_of_lt' (ha : a ≤ 0) (hbc : b < c) : a + b < c := -lt_of_le_of_lt (add_le_of_nonpos_of_le' ha (le_refl _)) hbc +@[to_additive] +lemma mul_lt_of_le_one_of_lt' (ha : a ≤ 1) (hbc : b < c) : a * b < c := +lt_of_le_of_lt (mul_le_of_le_one_of_le' ha (le_refl _)) hbc -lemma add_lt_of_lt_of_nonpos' (hbc : b < c) (ha : a ≤ 0) : b + a < c := -lt_of_le_of_lt (add_le_of_le_of_nonpos' (le_refl _) ha) hbc +@[to_additive] +lemma mul_lt_of_lt_of_le_one' (hbc : b < c) (ha : a ≤ 1) : b * a < c := +lt_of_le_of_lt (mul_le_of_le_of_le_one' (le_refl _) ha) hbc -lemma add_lt_of_neg_of_lt' (ha : a < 0) (hbc : b < c) : a + b < c := -add_lt_of_nonpos_of_lt' (le_of_lt ha) hbc +@[to_additive] +lemma mul_lt_of_lt_one_of_lt' (ha : a < 1) (hbc : b < c) : a * b < c := +mul_lt_of_le_one_of_lt' (le_of_lt ha) hbc -lemma add_lt_of_lt_of_neg' (hbc : b < c) (ha : a < 0) : b + a < c := -add_lt_of_lt_of_nonpos' hbc (le_of_lt ha) +@[to_additive] +lemma mul_lt_of_lt_of_lt_one' (hbc : b < c) (ha : a < 1) : b * a < c := +mul_lt_of_lt_of_le_one' hbc (le_of_lt ha) -lemma add_eq_zero_iff' (ha : 0 ≤ a) (hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0 := +@[to_additive] +lemma mul_eq_one_iff' (ha : 1 ≤ a) (hb : 1 ≤ b) : a * b = 1 ↔ a = 1 ∧ b = 1 := iff.intro - (assume hab : a + b = 0, - have a ≤ 0, from hab ▸ le_add_of_le_of_nonneg' (le_refl _) hb, - have a = 0, from le_antisymm this ha, - have b ≤ 0, from hab ▸ le_add_of_nonneg_of_le' ha (le_refl _), - have b = 0, from le_antisymm this hb, - and.intro ‹a = 0› ‹b = 0›) - (assume ⟨ha', hb'⟩, by rw [ha', hb', add_zero]) - -lemma bit0_pos {a : α} (h : 0 < a) : 0 < bit0 a := -add_pos' h h + (assume hab : a * b = 1, + have a ≤ 1, from hab ▸ le_mul_of_le_of_one_le' (le_refl _) hb, + have a = 1, from le_antisymm this ha, + have b ≤ 1, from hab ▸ le_mul_of_one_le_of_le' ha (le_refl _), + have b = 1, from le_antisymm this hb, + and.intro ‹a = 1› ‹b = 1›) + (assume ⟨ha', hb'⟩, by rw [ha', hb', mul_one]) section mono variables {β : Type*} [preorder β] {f g : β → α} -lemma monotone.add (hf : monotone f) (hg : monotone g) : monotone (λ x, f x + g x) := -λ x y h, add_le_add' (hf h) (hg h) +@[to_additive monotone.add] +lemma monotone.mul' (hf : monotone f) (hg : monotone g) : monotone (λ x, f x * g x) := +λ x y h, mul_le_mul' (hf h) (hg h) -lemma monotone.add_const (hf : monotone f) (a : α) : monotone (λ x, f x + a) := -hf.add monotone_const +@[to_additive monotone.add_const] +lemma monotone.mul_const' (hf : monotone f) (a : α) : monotone (λ x, f x * a) := +hf.mul' monotone_const -lemma monotone.const_add (hf : monotone f) (a : α) : monotone (λ x, a + f x) := -monotone_const.add hf +@[to_additive monotone.const_add] +lemma monotone.const_mul' (hf : monotone f) (a : α) : monotone (λ x, a * f x) := +monotone_const.mul' hf end mono -end ordered_add_comm_monoid +end ordered_comm_monoid + +lemma bit0_pos [ordered_add_comm_monoid α] {a : α} (h : 0 < a) : 0 < bit0 a := +add_pos' h h namespace units +@[to_additive] instance [monoid α] [i : preorder α] : preorder (units α) := preorder.lift (coe : units α → α) i -@[simp] theorem coe_le_coe [monoid α] [preorder α] {a b : units α} : +@[simp, to_additive] +theorem coe_le_coe [monoid α] [preorder α] {a b : units α} : (a : α) ≤ b ↔ a ≤ b := iff.rfl -@[simp] theorem coe_lt_coe [monoid α] [preorder α] {a b : units α} : +@[simp, to_additive] +theorem coe_lt_coe [monoid α] [preorder α] {a b : units α} : (a : α) < b ↔ a < b := iff.rfl +@[to_additive] instance [monoid α] [i : partial_order α] : partial_order (units α) := partial_order.lift (coe : units α → α) (by ext) i +@[to_additive] instance [monoid α] [i : linear_order α] : linear_order (units α) := linear_order.lift (coe : units α → α) (by ext) i +@[to_additive] instance [monoid α] [i : decidable_linear_order α] : decidable_linear_order (units α) := decidable_linear_order.lift (coe : units α → α) (by ext) i +@[simp, to_additive] theorem max_coe [monoid α] [decidable_linear_order α] {a b : units α} : (↑(max a b) : α) = max a b := by by_cases a ≤ b; simp [max, h] +@[simp, to_additive] theorem min_coe [monoid α] [decidable_linear_order α] {a b : units α} : (↑(min a b) : α) = min a b := by by_cases a ≤ b; simp [min, h] @@ -426,217 +488,321 @@ instance with_top.canonically_ordered_add_monoid : canonically_ordered_add_monoi end canonically_ordered_add_monoid -@[protect_proj] class ordered_cancel_add_comm_monoid (α : Type u) +/-- An ordered cancellative additive commutative monoid +is an additive commutative monoid with a partial order, +in which addition is cancellative and strictly monotone. -/ +@[protect_proj, ancestor add_comm_monoid add_left_cancel_semigroup add_right_cancel_semigroup partial_order] +class ordered_cancel_add_comm_monoid (α : Type u) extends add_comm_monoid α, add_left_cancel_semigroup α, add_right_cancel_semigroup α, partial_order α := (add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b) (le_of_add_le_add_left : ∀ a b c : α, a + b ≤ a + c → b ≤ c) -section ordered_cancel_add_comm_monoid -variables [ordered_cancel_add_comm_monoid α] {a b c d : α} - -lemma add_le_add_left : ∀ {a b : α} (h : a ≤ b) (c : α), c + a ≤ c + b := -ordered_cancel_add_comm_monoid.add_le_add_left - -lemma le_of_add_le_add_left : ∀ {a b c : α}, a + b ≤ a + c → b ≤ c := -ordered_cancel_add_comm_monoid.le_of_add_le_add_left - -lemma add_lt_add_left (h : a < b) (c : α) : c + a < c + b := -lt_of_le_not_le (add_le_add_left (le_of_lt h) _) $ - mt le_of_add_le_add_left (not_le_of_gt h) - -lemma lt_of_add_lt_add_left (h : a + b < a + c) : b < c := -lt_of_le_not_le (le_of_add_le_add_left (le_of_lt h)) $ - mt (λ h, add_le_add_left h _) (not_le_of_gt h) - -lemma add_le_add_right (h : a ≤ b) (c : α) : a + c ≤ b + c := -add_comm c a ▸ add_comm c b ▸ add_le_add_left h c - -theorem add_lt_add_right (h : a < b) (c : α) : a + c < b + c := +/-- An ordered cancellative commutative monoid +is a commutative monoid with a partial order, +in which multiplication is cancellative and strictly monotone. -/ +@[protect_proj, ancestor comm_monoid left_cancel_semigroup right_cancel_semigroup partial_order] +class ordered_cancel_comm_monoid (α : Type u) + extends comm_monoid α, left_cancel_semigroup α, + right_cancel_semigroup α, partial_order α := +(mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b) +(le_of_mul_le_mul_left : ∀ a b c : α, a * b ≤ a * c → b ≤ c) + +attribute [to_additive ordered_cancel_add_comm_monoid] ordered_cancel_comm_monoid + +section ordered_cancel_comm_monoid +variables [ordered_cancel_comm_monoid α] {a b c d : α} + +@[to_additive] +instance ordered_cancel_comm_monoid.to_left_cancel_monoid : + left_cancel_monoid α := { ..‹ordered_cancel_comm_monoid α› } + +@[to_additive add_le_add_left] +lemma mul_le_mul_left'' : ∀ {a b : α} (h : a ≤ b) (c : α), c * a ≤ c * b := +ordered_cancel_comm_monoid.mul_le_mul_left + +@[to_additive le_of_add_le_add_left] +lemma le_of_mul_le_mul_left' : ∀ {a b c : α}, a * b ≤ a * c → b ≤ c := +ordered_cancel_comm_monoid.le_of_mul_le_mul_left + +@[to_additive add_lt_add_left] +lemma mul_lt_mul_left' (h : a < b) (c : α) : c * a < c * b := +lt_of_le_not_le (mul_le_mul_left'' (le_of_lt h) _) $ + mt le_of_mul_le_mul_left' (not_le_of_gt h) + +@[to_additive lt_of_add_lt_add_left] +lemma lt_of_mul_lt_mul_left'' (h : a * b < a * c) : b < c := +lt_of_le_not_le (le_of_mul_le_mul_left' (le_of_lt h)) $ + mt (λ h, mul_le_mul_left'' h _) (not_le_of_gt h) + +@[to_additive] +instance ordered_cancel_comm_monoid.to_ordered_comm_monoid : ordered_comm_monoid α := +{ lt_of_mul_lt_mul_left := @lt_of_mul_lt_mul_left'' _ _, ..‹ordered_cancel_comm_monoid α› } + +@[to_additive add_le_add_right] +lemma mul_le_mul_right'' (h : a ≤ b) (c : α) : a * c ≤ b * c := +mul_comm c a ▸ mul_comm c b ▸ mul_le_mul_left' h + +@[to_additive add_lt_add_right] +lemma mul_lt_mul_right' (h : a < b) (c : α) : a * c < b * c := begin - rw [add_comm a c, add_comm b c], - exact (add_lt_add_left h c) + rw [mul_comm a c, mul_comm b c], + exact (mul_lt_mul_left' h c) end -lemma add_le_add {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d := -le_trans (add_le_add_right h₁ c) (add_le_add_left h₂ b) - -lemma le_add_of_nonneg_right (h : 0 ≤ b) : a ≤ a + b := -have a + 0 ≤ a + b, from add_le_add_left h a, -by rwa add_zero at this - -lemma le_add_of_nonneg_left (h : 0 ≤ b) : a ≤ b + a := -have 0 + a ≤ b + a, from add_le_add_right h a, -by rwa zero_add at this - -lemma add_lt_add (h₁ : a < b) (h₂ : c < d) : a + c < b + d := -lt_trans (add_lt_add_right h₁ c) (add_lt_add_left h₂ b) - -lemma add_lt_add_of_le_of_lt (h₁ : a ≤ b) (h₂ : c < d) : a + c < b + d := -lt_of_le_of_lt (add_le_add_right h₁ c) (add_lt_add_left h₂ b) - -lemma add_lt_add_of_lt_of_le (h₁ : a < b) (h₂ : c ≤ d) : a + c < b + d := -lt_of_lt_of_le (add_lt_add_right h₁ c) (add_le_add_left h₂ b) - -lemma lt_add_of_pos_right (a : α) {b : α} (h : 0 < b) : a < a + b := -have a + 0 < a + b, from add_lt_add_left h a, -by rwa [add_zero] at this - -lemma lt_add_of_pos_left (a : α) {b : α} (h : 0 < b) : a < b + a := -have 0 + a < b + a, from add_lt_add_right h a, -by rwa [zero_add] at this - -lemma le_of_add_le_add_right (h : a + b ≤ c + b) : a ≤ c := -le_of_add_le_add_left - (show b + a ≤ b + c, begin rw [add_comm b a, add_comm b c], assumption end) - -lemma lt_of_add_lt_add_right (h : a + b < c + b) : a < c := -lt_of_add_lt_add_left - (show b + a < b + c, begin rw [add_comm b a, add_comm b c], assumption end) - --- here we start using properties of zero. -lemma add_nonneg (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a + b := -zero_add (0:α) ▸ (add_le_add ha hb) - -lemma add_pos (ha : 0 < a) (hb : 0 < b) : 0 < a + b := - zero_add (0:α) ▸ (add_lt_add ha hb) - -lemma add_pos_of_pos_of_nonneg (ha : 0 < a) (hb : 0 ≤ b) : 0 < a + b := -zero_add (0:α) ▸ (add_lt_add_of_lt_of_le ha hb) - -lemma add_pos_of_nonneg_of_pos (ha : 0 ≤ a) (hb : 0 < b) : 0 < a + b := -zero_add (0:α) ▸ (add_lt_add_of_le_of_lt ha hb) - -lemma add_nonpos (ha : a ≤ 0) (hb : b ≤ 0) : a + b ≤ 0 := -zero_add (0:α) ▸ (add_le_add ha hb) - -lemma add_neg (ha : a < 0) (hb : b < 0) : a + b < 0 := -zero_add (0:α) ▸ (add_lt_add ha hb) - -lemma add_neg_of_neg_of_nonpos (ha : a < 0) (hb : b ≤ 0) : a + b < 0 := -zero_add (0:α) ▸ (add_lt_add_of_lt_of_le ha hb) - -lemma add_neg_of_nonpos_of_neg (ha : a ≤ 0) (hb : b < 0) : a + b < 0 := -zero_add (0:α) ▸ (add_lt_add_of_le_of_lt ha hb) - -lemma add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg - (ha : 0 ≤ a) (hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0 := +@[to_additive add_le_add] +lemma mul_le_mul'' {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) : a * c ≤ b * d := +le_trans (mul_le_mul_right' h₁) (mul_le_mul_left' h₂) + +@[to_additive] +lemma le_mul_of_one_le_right (h : 1 ≤ b) : a ≤ a * b := +have a * 1 ≤ a * b, from mul_le_mul_left' h, +by rwa mul_one at this + +@[to_additive] +lemma le_mul_of_one_le_left (h : 1 ≤ b) : a ≤ b * a := +have 1 * a ≤ b * a, from mul_le_mul_right' h, +by rwa one_mul at this + +@[to_additive add_lt_add] +lemma mul_lt_mul''' (h₁ : a < b) (h₂ : c < d) : a * c < b * d := +lt_trans (mul_lt_mul_right' h₁ c) (mul_lt_mul_left' h₂ b) + +@[to_additive] +lemma mul_lt_mul_of_le_of_lt (h₁ : a ≤ b) (h₂ : c < d) : a * c < b * d := +lt_of_le_of_lt (mul_le_mul_right' h₁) (mul_lt_mul_left' h₂ b) + +@[to_additive] +lemma mul_lt_mul_of_lt_of_le (h₁ : a < b) (h₂ : c ≤ d) : a * c < b * d := +lt_of_lt_of_le (mul_lt_mul_right' h₁ c) (mul_le_mul_left' h₂) + +@[to_additive] +lemma lt_mul_of_one_lt_right (a : α) {b : α} (h : 1 < b) : a < a * b := +have a * 1 < a * b, from mul_lt_mul_left' h a, +by rwa [mul_one] at this + +@[to_additive] +lemma lt_mul_of_one_lt_left (a : α) {b : α} (h : 1 < b) : a < b * a := +have 1 * a < b * a, from mul_lt_mul_right' h a, +by rwa [one_mul] at this + +@[to_additive le_of_add_le_add_right] +lemma le_of_mul_le_mul_right' (h : a * b ≤ c * b) : a ≤ c := +le_of_mul_le_mul_left' + (show b * a ≤ b * c, begin rw [mul_comm b a, mul_comm b c], assumption end) + +@[to_additive lt_of_add_lt_add_right] +lemma lt_of_mul_lt_mul_right'' (h : a * b < c * b) : a < c := +lt_of_mul_lt_mul_left'' + (show b * a < b * c, begin rw [mul_comm b a, mul_comm b c], assumption end) + +-- here we start using properties of one. +@[to_additive add_nonneg] +lemma one_le_mul (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ a * b := +one_mul (1:α) ▸ (mul_le_mul'' ha hb) + +@[to_additive] +lemma mul_one_lt (ha : 1 < a) (hb : 1 < b) : 1 < a * b := + one_mul (1:α) ▸ (mul_lt_mul''' ha hb) + +@[to_additive] +lemma mul_one_lt_of_one_lt_of_one_le (ha : 1 < a) (hb : 1 ≤ b) : 1 < a * b := +one_mul (1:α) ▸ (mul_lt_mul_of_lt_of_le ha hb) + +@[to_additive] +lemma mul_one_lt_of_one_le_of_one_lt (ha : 1 ≤ a) (hb : 1 < b) : 1 < a * b := +one_mul (1:α) ▸ (mul_lt_mul_of_le_of_lt ha hb) + +@[to_additive add_nonpos] +lemma mul_le_one'' (ha : a ≤ 1) (hb : b ≤ 1) : a * b ≤ 1 := +one_mul (1:α) ▸ (mul_le_mul'' ha hb) + +@[to_additive] +lemma mul_lt_one (ha : a < 1) (hb : b < 1) : a * b < 1 := +one_mul (1:α) ▸ (mul_lt_mul''' ha hb) + +@[to_additive] +lemma mul_lt_one_of_lt_one_of_le_one (ha : a < 1) (hb : b ≤ 1) : a * b < 1 := +one_mul (1:α) ▸ (mul_lt_mul_of_lt_of_le ha hb) + +@[to_additive] +lemma mul_lt_one_of_le_one_of_lt_one (ha : a ≤ 1) (hb : b < 1) : a * b < 1 := +one_mul (1:α) ▸ (mul_lt_mul_of_le_of_lt ha hb) + +@[to_additive] +lemma mul_eq_one_iff_eq_one_and_eq_one_of_one_le_of_one_le + (ha : 1 ≤ a) (hb : 1 ≤ b) : a * b = 1 ↔ a = 1 ∧ b = 1 := iff.intro - (assume hab : a + b = 0, - have ha' : a ≤ 0, from + (assume hab : a * b = 1, + have ha' : a ≤ 1, from calc - a = a + 0 : by rw add_zero - ... ≤ a + b : add_le_add_left hb _ - ... = 0 : hab, - have haz : a = 0, from le_antisymm ha' ha, - have hb' : b ≤ 0, from + a = a * 1 : by rw mul_one + ... ≤ a * b : mul_le_mul_left' hb + ... = 1 : hab, + have haz : a = 1, from le_antisymm ha' ha, + have hb' : b ≤ 1, from calc - b = 0 + b : by rw zero_add - ... ≤ a + b : by exact add_le_add_right ha _ - ... = 0 : hab, - have hbz : b = 0, from le_antisymm hb' hb, + b = 1 * b : by rw one_mul + ... ≤ a * b : by exact mul_le_mul_right' ha + ... = 1 : hab, + have hbz : b = 1, from le_antisymm hb' hb, and.intro haz hbz) (assume ⟨ha', hb'⟩, - by rw [ha', hb', add_zero]) - -lemma le_add_of_nonneg_of_le (ha : 0 ≤ a) (hbc : b ≤ c) : b ≤ a + c := -zero_add b ▸ add_le_add ha hbc - -lemma le_add_of_le_of_nonneg (hbc : b ≤ c) (ha : 0 ≤ a) : b ≤ c + a := -add_zero b ▸ add_le_add hbc ha - -lemma lt_add_of_pos_of_le (ha : 0 < a) (hbc : b ≤ c) : b < a + c := -zero_add b ▸ add_lt_add_of_lt_of_le ha hbc - -lemma lt_add_of_le_of_pos (hbc : b ≤ c) (ha : 0 < a) : b < c + a := -add_zero b ▸ add_lt_add_of_le_of_lt hbc ha - -lemma add_le_of_nonpos_of_le (ha : a ≤ 0) (hbc : b ≤ c) : a + b ≤ c := -zero_add c ▸ add_le_add ha hbc - -lemma add_le_of_le_of_nonpos (hbc : b ≤ c) (ha : a ≤ 0) : b + a ≤ c := -add_zero c ▸ add_le_add hbc ha - -lemma add_lt_of_neg_of_le (ha : a < 0) (hbc : b ≤ c) : a + b < c := -zero_add c ▸ add_lt_add_of_lt_of_le ha hbc - -lemma add_lt_of_le_of_neg (hbc : b ≤ c) (ha : a < 0) : b + a < c := -add_zero c ▸ add_lt_add_of_le_of_lt hbc ha - -lemma lt_add_of_nonneg_of_lt (ha : 0 ≤ a) (hbc : b < c) : b < a + c := -zero_add b ▸ add_lt_add_of_le_of_lt ha hbc - -lemma lt_add_of_lt_of_nonneg (hbc : b < c) (ha : 0 ≤ a) : b < c + a := -add_zero b ▸ add_lt_add_of_lt_of_le hbc ha - -lemma lt_add_of_pos_of_lt (ha : 0 < a) (hbc : b < c) : b < a + c := -zero_add b ▸ add_lt_add ha hbc + by rw [ha', hb', mul_one]) -lemma lt_add_of_lt_of_pos (hbc : b < c) (ha : 0 < a) : b < c + a := -add_zero b ▸ add_lt_add hbc ha +@[to_additive] +lemma le_mul_of_one_le_of_le (ha : 1 ≤ a) (hbc : b ≤ c) : b ≤ a * c := +one_mul b ▸ mul_le_mul'' ha hbc -lemma add_lt_of_nonpos_of_lt (ha : a ≤ 0) (hbc : b < c) : a + b < c := -zero_add c ▸ add_lt_add_of_le_of_lt ha hbc +@[to_additive] +lemma le_mul_of_le_of_one_le (hbc : b ≤ c) (ha : 1 ≤ a) : b ≤ c * a := +mul_one b ▸ mul_le_mul'' hbc ha -lemma add_lt_of_lt_of_nonpos (hbc : b < c) (ha : a ≤ 0) : b + a < c := -add_zero c ▸ add_lt_add_of_lt_of_le hbc ha +@[to_additive] +lemma lt_mul_of_one_lt_of_le (ha : 1 < a) (hbc : b ≤ c) : b < a * c := +one_mul b ▸ mul_lt_mul_of_lt_of_le ha hbc -lemma add_lt_of_neg_of_lt (ha : a < 0) (hbc : b < c) : a + b < c := -zero_add c ▸ add_lt_add ha hbc +@[to_additive] +lemma lt_mul_of_le_of_one_lt (hbc : b ≤ c) (ha : 1 < a) : b < c * a := +mul_one b ▸ mul_lt_mul_of_le_of_lt hbc ha -lemma add_lt_of_lt_of_neg (hbc : b < c) (ha : a < 0) : b + a < c := -add_zero c ▸ add_lt_add hbc ha - -instance ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid : ordered_add_comm_monoid α := -{ lt_of_add_lt_add_left := @lt_of_add_lt_add_left _ _, ..‹ordered_cancel_add_comm_monoid α› } - -instance ordered_cancel_add_comm_monoid.to_add_left_cancel_monoid : - add_left_cancel_monoid α := { ..‹ordered_cancel_add_comm_monoid α› } - -@[simp] lemma add_le_add_iff_left (a : α) {b c : α} : a + b ≤ a + c ↔ b ≤ c := -⟨le_of_add_le_add_left, λ h, add_le_add_left h _⟩ - -@[simp] lemma add_le_add_iff_right (c : α) : a + c ≤ b + c ↔ a ≤ b := -add_comm c a ▸ add_comm c b ▸ add_le_add_iff_left c - -@[simp] lemma add_lt_add_iff_left (a : α) {b c : α} : a + b < a + c ↔ b < c := -⟨lt_of_add_lt_add_left, λ h, add_lt_add_left h _⟩ +@[to_additive] +lemma mul_le_of_le_one_of_le (ha : a ≤ 1) (hbc : b ≤ c) : a * b ≤ c := +one_mul c ▸ mul_le_mul'' ha hbc + +@[to_additive] +lemma mul_le_of_le_of_le_one (hbc : b ≤ c) (ha : a ≤ 1) : b * a ≤ c := +mul_one c ▸ mul_le_mul'' hbc ha + +@[to_additive] +lemma mul_lt_of_lt_one_of_le (ha : a < 1) (hbc : b ≤ c) : a * b < c := +one_mul c ▸ mul_lt_mul_of_lt_of_le ha hbc + +@[to_additive] +lemma mul_lt_of_le_of_lt_one (hbc : b ≤ c) (ha : a < 1) : b * a < c := +mul_one c ▸ mul_lt_mul_of_le_of_lt hbc ha + +@[to_additive] +lemma lt_mul_of_one_le_of_lt (ha : 1 ≤ a) (hbc : b < c) : b < a * c := +one_mul b ▸ mul_lt_mul_of_le_of_lt ha hbc + +@[to_additive] +lemma lt_mul_of_lt_of_one_le (hbc : b < c) (ha : 1 ≤ a) : b < c * a := +mul_one b ▸ mul_lt_mul_of_lt_of_le hbc ha + +@[to_additive] +lemma lt_mul_of_one_lt_of_lt (ha : 1 < a) (hbc : b < c) : b < a * c := +one_mul b ▸ mul_lt_mul''' ha hbc + +@[to_additive] +lemma lt_mul_of_lt_of_one_lt (hbc : b < c) (ha : 1 < a) : b < c * a := +mul_one b ▸ mul_lt_mul''' hbc ha + +@[to_additive] +lemma mul_lt_of_le_one_of_lt (ha : a ≤ 1) (hbc : b < c) : a * b < c := +one_mul c ▸ mul_lt_mul_of_le_of_lt ha hbc + +@[to_additive] +lemma mul_lt_of_lt_of_le_one (hbc : b < c) (ha : a ≤ 1) : b * a < c := +mul_one c ▸ mul_lt_mul_of_lt_of_le hbc ha + +@[to_additive] +lemma mul_lt_of_lt_one_of_lt (ha : a < 1) (hbc : b < c) : a * b < c := +one_mul c ▸ mul_lt_mul''' ha hbc + +@[to_additive] +lemma mul_lt_of_lt_of_lt_one (hbc : b < c) (ha : a < 1) : b * a < c := +mul_one c ▸ mul_lt_mul''' hbc ha + +@[simp, to_additive] +lemma mul_le_mul_iff_left (a : α) {b c : α} : a * b ≤ a * c ↔ b ≤ c := +⟨le_of_mul_le_mul_left', λ h, mul_le_mul_left' h⟩ + +@[simp, to_additive] +lemma mul_le_mul_iff_right (c : α) : a * c ≤ b * c ↔ a ≤ b := +mul_comm c a ▸ mul_comm c b ▸ mul_le_mul_iff_left c + +@[simp, to_additive] +lemma mul_lt_mul_iff_left (a : α) {b c : α} : a * b < a * c ↔ b < c := +⟨lt_of_mul_lt_mul_left'', λ h, mul_lt_mul_left' h _⟩ + +@[simp, to_additive] +lemma mul_lt_mul_iff_right (c : α) : a * c < b * c ↔ a < b := +mul_comm c a ▸ mul_comm c b ▸ mul_lt_mul_iff_left c + +@[simp, to_additive le_add_iff_nonneg_right] +lemma le_mul_iff_one_le_right' (a : α) {b : α} : a ≤ a * b ↔ 1 ≤ b := +have a * 1 ≤ a * b ↔ 1 ≤ b, from mul_le_mul_iff_left a, +by rwa mul_one at this + +@[simp, to_additive le_add_iff_nonneg_left] +lemma le_mul_iff_one_le_left' (a : α) {b : α} : a ≤ b * a ↔ 1 ≤ b := +by rw [mul_comm, le_mul_iff_one_le_right'] + +@[simp, to_additive lt_add_iff_pos_right] +lemma lt_mul_iff_one_lt_right' (a : α) {b : α} : a < a * b ↔ 1 < b := +have a * 1 < a * b ↔ 1 < b, from mul_lt_mul_iff_left a, +by rwa mul_one at this + +@[simp, to_additive lt_add_iff_pos_left] +lemma lt_mul_iff_one_lt_left' (a : α) {b : α} : a < b * a ↔ 1 < b := +by rw [mul_comm, lt_mul_iff_one_lt_right'] + +@[simp, to_additive add_le_iff_nonpos_left] +lemma mul_le_iff_le_one_left' : a * b ≤ b ↔ a ≤ 1 := +by { convert mul_le_mul_iff_right b, rw [one_mul] } + +@[simp, to_additive add_le_iff_nonpos_right] +lemma mul_le_iff_le_one_right' : a * b ≤ a ↔ b ≤ 1 := +by { convert mul_le_mul_iff_left a, rw [mul_one] } + +@[simp, to_additive add_lt_iff_neg_right] +lemma mul_lt_iff_lt_one_right' : a * b < b ↔ a < 1 := +by { convert mul_lt_mul_iff_right b, rw [one_mul] } + +@[simp, to_additive add_lt_iff_neg_left] +lemma mul_lt_iff_lt_one_left' : a * b < a ↔ b < 1 := +by { convert mul_lt_mul_iff_left a, rw [mul_one] } + +@[to_additive] +lemma mul_eq_one_iff_eq_one_of_one_le + (ha : 1 ≤ a) (hb : 1 ≤ b) : a * b = 1 ↔ a = 1 ∧ b = 1 := +⟨λ hab : a * b = 1, +by split; apply le_antisymm; try {assumption}; + rw ← hab; simp [ha, hb], +λ ⟨ha', hb'⟩, by rw [ha', hb', mul_one]⟩ -@[simp] lemma add_lt_add_iff_right (c : α) : a + c < b + c ↔ a < b := -add_comm c a ▸ add_comm c b ▸ add_lt_add_iff_left c +section mono -@[simp] lemma le_add_iff_nonneg_right (a : α) {b : α} : a ≤ a + b ↔ 0 ≤ b := -have a + 0 ≤ a + b ↔ 0 ≤ b, from add_le_add_iff_left a, -by rwa add_zero at this +variables {β : Type*} [preorder β] {f g : β → α} -@[simp] lemma le_add_iff_nonneg_left (a : α) {b : α} : a ≤ b + a ↔ 0 ≤ b := -by rw [add_comm, le_add_iff_nonneg_right] +@[to_additive monotone.add_strict_mono] +lemma monotone.mul_strict_mono' (hf : monotone f) (hg : strict_mono g) : + strict_mono (λ x, f x * g x) := +λ x y h, mul_lt_mul_of_le_of_lt (hf $ le_of_lt h) (hg h) -@[simp] lemma lt_add_iff_pos_right (a : α) {b : α} : a < a + b ↔ 0 < b := -have a + 0 < a + b ↔ 0 < b, from add_lt_add_iff_left a, -by rwa add_zero at this +@[to_additive strict_mono.add_monotone] +lemma strict_mono.mul_monotone' (hf : strict_mono f) (hg : monotone g) : + strict_mono (λ x, f x * g x) := +λ x y h, mul_lt_mul_of_lt_of_le (hf h) (hg $ le_of_lt h) -@[simp] lemma lt_add_iff_pos_left (a : α) {b : α} : a < b + a ↔ 0 < b := -by rw [add_comm, lt_add_iff_pos_right] +@[to_additive strict_mono.add_const] +lemma strict_mono.mul_const' (hf : strict_mono f) (c : α) : + strict_mono (λ x, f x * c) := +hf.mul_monotone' monotone_const -@[simp] lemma add_le_iff_nonpos_left : a + b ≤ b ↔ a ≤ 0 := -by { convert add_le_add_iff_right b, rw [zero_add] } +@[to_additive strict_mono.const_add] +lemma strict_mono.const_mul' (hf : strict_mono f) (c : α) : + strict_mono (λ x, c * f x) := +monotone_const.mul_strict_mono' hf -@[simp] lemma add_le_iff_nonpos_right : a + b ≤ a ↔ b ≤ 0 := -by { convert add_le_add_iff_left a, rw [add_zero] } +end mono -@[simp] lemma add_lt_iff_neg_right : a + b < b ↔ a < 0 := -by { convert add_lt_add_iff_right b, rw [zero_add] } +end ordered_cancel_comm_monoid -@[simp] lemma add_lt_iff_neg_left : a + b < a ↔ b < 0 := -by { convert add_lt_add_iff_left a, rw [add_zero] } +section ordered_cancel_add_comm_monoid -lemma add_eq_zero_iff_eq_zero_of_nonneg - (ha : 0 ≤ a) (hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0 := -⟨λ hab : a + b = 0, -by split; apply le_antisymm; try {assumption}; - rw ← hab; simp [ha, hb], -λ ⟨ha', hb'⟩, by rw [ha', hb', add_zero]⟩ +variable [ordered_cancel_add_comm_monoid α] lemma with_top.add_lt_add_iff_left : ∀{a b c : with_top α}, a < ⊤ → (a + c < a + b ↔ c < b) @@ -655,137 +821,355 @@ lemma with_top.add_lt_add_iff_right {a b c : with_top α} : a < ⊤ → (c + a < b + a ↔ c < b) := by simpa [add_comm] using @with_top.add_lt_add_iff_left _ _ a b c -section mono - -variables {β : Type*} [preorder β] {f g : β → α} - -lemma monotone.add_strict_mono (hf : monotone f) (hg : strict_mono g) : - strict_mono (λ x, f x + g x) := -λ x y h, add_lt_add_of_le_of_lt (hf $ le_of_lt h) (hg h) - -lemma strict_mono.add_monotone (hf : strict_mono f) (hg : monotone g) : - strict_mono (λ x, f x + g x) := -λ x y h, add_lt_add_of_lt_of_le (hf h) (hg $ le_of_lt h) - -lemma strict_mono.add_const (hf : strict_mono f) (c : α) : - strict_mono (λ x, f x + c) := -hf.add_monotone monotone_const - -lemma strict_mono.const_add (hf : strict_mono f) (c : α) : - strict_mono (λ x, c + f x) := -monotone_const.add_strict_mono hf - -end mono - end ordered_cancel_add_comm_monoid -@[protect_proj] +/-- An ordered additive commutative group is an additive commutative group +with a partial order in which addition is strictly monotone. -/ +@[protect_proj, ancestor add_comm_group partial_order] class ordered_add_comm_group (α : Type u) extends add_comm_group α, partial_order α := (add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b) -section ordered_add_comm_group -variables [ordered_add_comm_group α] {a b c d : α} +/-- An ordered commutative group is an commutative group +with a partial order in which multiplication is strictly monotone. -/ +@[protect_proj, ancestor comm_group partial_order] +class ordered_comm_group (α : Type u) extends comm_group α, partial_order α := +(mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b) + +attribute [to_additive ordered_add_comm_group] ordered_comm_group -lemma ordered_add_comm_group.add_lt_add_left (a b : α) (h : a < b) (c : α) : c + a < c + b := +section ordered_comm_group +variables [ordered_comm_group α] {a b c d : α} + +@[to_additive ordered_add_comm_group.add_lt_add_left] +lemma ordered_comm_group.mul_lt_mul_left' (a b : α) (h : a < b) (c : α) : c * a < c * b := begin rw lt_iff_le_not_le at h ⊢, split, - { apply ordered_add_comm_group.add_le_add_left _ _ h.1 }, + { apply ordered_comm_group.mul_le_mul_left _ _ h.1 }, { intro w, - have w : -c + (c + b) ≤ -c + (c + a) := ordered_add_comm_group.add_le_add_left _ _ w _, - simp only [add_zero, add_comm, add_left_neg, add_left_comm] at w, + replace w : c⁻¹ * (c * b) ≤ c⁻¹ * (c * a) := ordered_comm_group.mul_le_mul_left _ _ w _, + simp only [mul_one, mul_comm, mul_left_inv, mul_left_comm] at w, exact h.2 w }, end -lemma ordered_add_comm_group.le_of_add_le_add_left (h : a + b ≤ a + c) : b ≤ c := -have -a + (a + b) ≤ -a + (a + c), from ordered_add_comm_group.add_le_add_left _ _ h _, -begin simp [neg_add_cancel_left] at this, assumption end - -lemma ordered_add_comm_group.lt_of_add_lt_add_left (h : a + b < a + c) : b < c := -have -a + (a + b) < -a + (a + c), from ordered_add_comm_group.add_lt_add_left _ _ h _, -begin simp [neg_add_cancel_left] at this, assumption end - -instance ordered_add_comm_group.to_ordered_cancel_add_comm_monoid (α : Type u) - [s : ordered_add_comm_group α] : ordered_cancel_add_comm_monoid α := -{ add_left_cancel := @add_left_cancel α _, - add_right_cancel := @add_right_cancel α _, - le_of_add_le_add_left := @ordered_add_comm_group.le_of_add_le_add_left α _, +@[to_additive ordered_add_comm_group.le_of_add_le_add_left] +lemma ordered_comm_group.le_of_mul_le_mul_left (h : a * b ≤ a * c) : b ≤ c := +have a⁻¹ * (a * b) ≤ a⁻¹ * (a * c), from ordered_comm_group.mul_le_mul_left _ _ h _, +begin simp [inv_mul_cancel_left] at this, assumption end + +@[to_additive] +lemma ordered_comm_group.lt_of_mul_lt_mul_left (h : a * b < a * c) : b < c := +have a⁻¹ * (a * b) < a⁻¹ * (a * c), from ordered_comm_group.mul_lt_mul_left' _ _ h _, +begin simp [inv_mul_cancel_left] at this, assumption end + +@[to_additive] +instance ordered_comm_group.to_ordered_cancel_comm_monoid (α : Type u) + [s : ordered_comm_group α] : ordered_cancel_comm_monoid α := +{ mul_left_cancel := @mul_left_cancel α _, + mul_right_cancel := @mul_right_cancel α _, + le_of_mul_le_mul_left := @ordered_comm_group.le_of_mul_le_mul_left α _, ..s } -lemma neg_le_neg (h : a ≤ b) : -b ≤ -a := -have 0 ≤ -a + b, from add_left_neg a ▸ add_le_add_left h (-a), -have 0 + -b ≤ -a + b + -b, from add_le_add_right this (-b), -by rwa [add_neg_cancel_right, zero_add] at this +@[to_additive neg_le_neg] +lemma inv_le_inv' (h : a ≤ b) : b⁻¹ ≤ a⁻¹ := +have 1 ≤ a⁻¹ * b, from mul_left_inv a ▸ mul_le_mul_left' h, +have 1 * b⁻¹ ≤ a⁻¹ * b * b⁻¹, from mul_le_mul_right' this, +by rwa [mul_inv_cancel_right, one_mul] at this + +@[to_additive] +lemma le_of_inv_le_inv (h : b⁻¹ ≤ a⁻¹) : a ≤ b := +suffices (a⁻¹)⁻¹ ≤ (b⁻¹)⁻¹, from + begin simp [inv_inv] at this, assumption end, +inv_le_inv' h + +@[to_additive] +lemma one_le_of_inv_le_one (h : a⁻¹ ≤ 1) : 1 ≤ a := +have a⁻¹ ≤ 1⁻¹, by rwa one_inv, +le_of_inv_le_inv this + +@[to_additive] +lemma inv_le_one_of_one_le (h : 1 ≤ a) : a⁻¹ ≤ 1 := +have a⁻¹ ≤ 1⁻¹, from inv_le_inv' h, +by rwa one_inv at this + +@[to_additive nonpos_of_neg_nonneg] +lemma le_one_of_one_le_inv (h : 1 ≤ a⁻¹) : a ≤ 1 := +have 1⁻¹ ≤ a⁻¹, by rwa one_inv, +le_of_inv_le_inv this + +@[to_additive neg_nonneg_of_nonpos] +lemma one_le_inv_of_le_one (h : a ≤ 1) : 1 ≤ a⁻¹ := +have 1⁻¹ ≤ a⁻¹, from inv_le_inv' h, +by rwa one_inv at this + +@[to_additive neg_lt_neg] +lemma inv_lt_inv' (h : a < b) : b⁻¹ < a⁻¹ := +have 1 < a⁻¹ * b, from mul_left_inv a ▸ mul_lt_mul_left' h (a⁻¹), +have 1 * b⁻¹ < a⁻¹ * b * b⁻¹, from mul_lt_mul_right' this (b⁻¹), +by rwa [mul_inv_cancel_right, one_mul] at this + +@[to_additive] +lemma lt_of_inv_lt_inv (h : b⁻¹ < a⁻¹) : a < b := +inv_inv a ▸ inv_inv b ▸ inv_lt_inv' h + +@[to_additive] +lemma one_lt_of_inv_inv (h : a⁻¹ < 1) : 1 < a := +have a⁻¹ < 1⁻¹, by rwa one_inv, +lt_of_inv_lt_inv this + +@[to_additive] +lemma inv_inv_of_one_lt (h : 1 < a) : a⁻¹ < 1 := +have a⁻¹ < 1⁻¹, from inv_lt_inv' h, +by rwa one_inv at this + +@[to_additive neg_of_neg_pos] +lemma inv_of_one_lt_inv (h : 1 < a⁻¹) : a < 1 := +have 1⁻¹ < a⁻¹, by rwa one_inv, +lt_of_inv_lt_inv this + +@[to_additive neg_pos_of_neg] +lemma one_lt_inv_of_inv (h : a < 1) : 1 < a⁻¹ := +have 1⁻¹ < a⁻¹, from inv_lt_inv' h, +by rwa one_inv at this + +@[to_additive] +lemma le_inv_of_le_inv (h : a ≤ b⁻¹) : b ≤ a⁻¹ := +begin + have h := inv_le_inv' h, + rwa inv_inv at h +end -lemma le_of_neg_le_neg (h : -b ≤ -a) : a ≤ b := -suffices -(-a) ≤ -(-b), from - begin simp [neg_neg] at this, assumption end, -neg_le_neg h +@[to_additive] +lemma inv_le_of_inv_le (h : a⁻¹ ≤ b) : b⁻¹ ≤ a := +begin + have h := inv_le_inv' h, + rwa inv_inv at h +end -lemma nonneg_of_neg_nonpos (h : -a ≤ 0) : 0 ≤ a := -have -a ≤ -0, by rwa neg_zero, -le_of_neg_le_neg this +@[to_additive] +lemma lt_inv_of_lt_inv (h : a < b⁻¹) : b < a⁻¹ := +begin + have h := inv_lt_inv' h, + rwa inv_inv at h +end -lemma neg_nonpos_of_nonneg (h : 0 ≤ a) : -a ≤ 0 := -have -a ≤ -0, from neg_le_neg h, -by rwa neg_zero at this +@[to_additive] +lemma inv_lt_of_inv_lt (h : a⁻¹ < b) : b⁻¹ < a := +begin + have h := inv_lt_inv' h, + rwa inv_inv at h +end -lemma nonpos_of_neg_nonneg (h : 0 ≤ -a) : a ≤ 0 := -have -0 ≤ -a, by rwa neg_zero, -le_of_neg_le_neg this +@[to_additive] +lemma mul_le_of_le_inv_mul (h : b ≤ a⁻¹ * c) : a * b ≤ c := +begin + have h := mul_le_mul_left' h, + rwa mul_inv_cancel_left at h +end -lemma neg_nonneg_of_nonpos (h : a ≤ 0) : 0 ≤ -a := -have -0 ≤ -a, from neg_le_neg h, -by rwa neg_zero at this +@[to_additive] +lemma le_inv_mul_of_mul_le (h : a * b ≤ c) : b ≤ a⁻¹ * c := +begin + have h := mul_le_mul_left' h, + rwa inv_mul_cancel_left at h +end -lemma neg_lt_neg (h : a < b) : -b < -a := -have 0 < -a + b, from add_left_neg a ▸ add_lt_add_left h (-a), -have 0 + -b < -a + b + -b, from add_lt_add_right this (-b), -by rwa [add_neg_cancel_right, zero_add] at this +@[to_additive] +lemma le_mul_of_inv_mul_le (h : b⁻¹ * a ≤ c) : a ≤ b * c := +begin + have h := mul_le_mul_left' h, + rwa mul_inv_cancel_left at h +end -lemma lt_of_neg_lt_neg (h : -b < -a) : a < b := -neg_neg a ▸ neg_neg b ▸ neg_lt_neg h +@[to_additive] +lemma inv_mul_le_of_le_mul (h : a ≤ b * c) : b⁻¹ * a ≤ c := +begin + have h := mul_le_mul_left' h, + rwa inv_mul_cancel_left at h +end -lemma pos_of_neg_neg (h : -a < 0) : 0 < a := -have -a < -0, by rwa neg_zero, -lt_of_neg_lt_neg this +@[to_additive] +lemma le_mul_of_inv_mul_le_left (h : b⁻¹ * a ≤ c) : a ≤ b * c := +le_mul_of_inv_mul_le h -lemma neg_neg_of_pos (h : 0 < a) : -a < 0 := -have -a < -0, from neg_lt_neg h, -by rwa neg_zero at this +@[to_additive] +lemma inv_mul_le_left_of_le_mul (h : a ≤ b * c) : b⁻¹ * a ≤ c := +inv_mul_le_of_le_mul h -lemma neg_of_neg_pos (h : 0 < -a) : a < 0 := -have -0 < -a, by rwa neg_zero, -lt_of_neg_lt_neg this +@[to_additive] +lemma le_mul_of_inv_mul_le_right (h : c⁻¹ * a ≤ b) : a ≤ b * c := +by { rw mul_comm, exact le_mul_of_inv_mul_le h } -lemma neg_pos_of_neg (h : a < 0) : 0 < -a := -have -0 < -a, from neg_lt_neg h, -by rwa neg_zero at this +@[to_additive] +lemma inv_mul_le_right_of_le_mul (h : a ≤ b * c) : c⁻¹ * a ≤ b := +by { rw mul_comm at h, apply inv_mul_le_left_of_le_mul h } -lemma le_neg_of_le_neg (h : a ≤ -b) : b ≤ -a := +@[to_additive] +lemma mul_lt_of_lt_inv_mul (h : b < a⁻¹ * c) : a * b < c := begin - have h := neg_le_neg h, - rwa neg_neg at h + have h := mul_lt_mul_left' h a, + rwa mul_inv_cancel_left at h end -lemma neg_le_of_neg_le (h : -a ≤ b) : -b ≤ a := +@[to_additive] +lemma lt_inv_mul_of_mul_lt (h : a * b < c) : b < a⁻¹ * c := begin - have h := neg_le_neg h, - rwa neg_neg at h + have h := mul_lt_mul_left' h (a⁻¹), + rwa inv_mul_cancel_left at h end -lemma lt_neg_of_lt_neg (h : a < -b) : b < -a := +@[to_additive] +lemma lt_mul_of_inv_mul_lt (h : b⁻¹ * a < c) : a < b * c := begin - have h := neg_lt_neg h, - rwa neg_neg at h + have h := mul_lt_mul_left' h b, + rwa mul_inv_cancel_left at h end -lemma neg_lt_of_neg_lt (h : -a < b) : -b < a := +@[to_additive] +lemma inv_mul_lt_of_lt_mul (h : a < b * c) : b⁻¹ * a < c := begin - have h := neg_lt_neg h, - rwa neg_neg at h + have h := mul_lt_mul_left' h (b⁻¹), + rwa inv_mul_cancel_left at h end +@[to_additive] +lemma lt_mul_of_inv_mul_lt_left (h : b⁻¹ * a < c) : a < b * c := +lt_mul_of_inv_mul_lt h + +@[to_additive] +lemma inv_mul_lt_left_of_lt_mul (h : a < b * c) : b⁻¹ * a < c := +inv_mul_lt_of_lt_mul h + +@[to_additive] +lemma lt_mul_of_inv_mul_lt_right (h : c⁻¹ * a < b) : a < b * c := +by { rw mul_comm, exact lt_mul_of_inv_mul_lt h } + +@[to_additive] +lemma inv_mul_lt_right_of_lt_mul (h : a < b * c) : c⁻¹ * a < b := +by { rw mul_comm at h, exact inv_mul_lt_of_lt_mul h } + +@[to_additive] +lemma mul_le_mul_three {a b c d e f : α} (h₁ : a ≤ d) (h₂ : b ≤ e) (h₃ : c ≤ f) : + a * b * c ≤ d * e * f := +begin + apply le_trans, + apply mul_le_mul'', + apply mul_le_mul'', + assumption', + apply le_refl +end + +@[simp, to_additive] +lemma inv_lt_one_iff_one_lt : a⁻¹ < 1 ↔ 1 < a := +⟨ one_lt_of_inv_inv, inv_inv_of_one_lt ⟩ + +@[simp, to_additive] +lemma inv_le_inv_iff : a⁻¹ ≤ b⁻¹ ↔ b ≤ a := +have a * b * a⁻¹ ≤ a * b * b⁻¹ ↔ a⁻¹ ≤ b⁻¹, from mul_le_mul_iff_left _, +by { rw [mul_inv_cancel_right, mul_comm a, mul_inv_cancel_right] at this, rw [this] } + +@[to_additive neg_le] +lemma inv_le' : a⁻¹ ≤ b ↔ b⁻¹ ≤ a := +have a⁻¹ ≤ (b⁻¹)⁻¹ ↔ b⁻¹ ≤ a, from inv_le_inv_iff, +by rwa inv_inv at this + +@[to_additive le_neg] +lemma le_inv' : a ≤ b⁻¹ ↔ b ≤ a⁻¹ := +have (a⁻¹)⁻¹ ≤ b⁻¹ ↔ b ≤ a⁻¹, from inv_le_inv_iff, +by rwa inv_inv at this + +@[to_additive neg_le_iff_add_nonneg] +lemma inv_le_iff_one_le_mul : a⁻¹ ≤ b ↔ 1 ≤ a * b := +(mul_le_mul_iff_left a).symm.trans $ by rw mul_inv_self + +@[to_additive] +lemma le_inv_iff_mul_le_one : a ≤ b⁻¹ ↔ a * b ≤ 1 := +(mul_le_mul_iff_right b).symm.trans $ by rw inv_mul_self + +@[simp, to_additive neg_nonpos] +lemma inv_le_one' : a⁻¹ ≤ 1 ↔ 1 ≤ a := +have a⁻¹ ≤ 1⁻¹ ↔ 1 ≤ a, from inv_le_inv_iff, +by rwa one_inv at this + +@[simp, to_additive neg_nonneg] +lemma one_le_inv' : 1 ≤ a⁻¹ ↔ a ≤ 1 := +have 1⁻¹ ≤ a⁻¹ ↔ a ≤ 1, from inv_le_inv_iff, +by rwa one_inv at this + +@[to_additive] +lemma inv_le_self (h : 1 ≤ a) : a⁻¹ ≤ a := +le_trans (inv_le_one'.2 h) h + +@[to_additive] +lemma self_le_inv (h : a ≤ 1) : a ≤ a⁻¹ := +le_trans h (one_le_inv'.2 h) + +@[simp, to_additive] +lemma inv_lt_inv_iff : a⁻¹ < b⁻¹ ↔ b < a := +have a * b * a⁻¹ < a * b * b⁻¹ ↔ a⁻¹ < b⁻¹, from mul_lt_mul_iff_left _, +by { rw [mul_inv_cancel_right, mul_comm a, mul_inv_cancel_right] at this, rw [this] } + +@[to_additive neg_lt_zero] +lemma inv_lt_one' : a⁻¹ < 1 ↔ 1 < a := +have a⁻¹ < 1⁻¹ ↔ 1 < a, from inv_lt_inv_iff, +by rwa one_inv at this + +@[to_additive neg_pos] +lemma one_lt_inv' : 1 < a⁻¹ ↔ a < 1 := +have 1⁻¹ < a⁻¹ ↔ a < 1, from inv_lt_inv_iff, +by rwa one_inv at this + +@[to_additive neg_lt] +lemma inv_lt' : a⁻¹ < b ↔ b⁻¹ < a := +have a⁻¹ < (b⁻¹)⁻¹ ↔ b⁻¹ < a, from inv_lt_inv_iff, +by rwa inv_inv at this + +@[to_additive lt_neg] +lemma lt_inv' : a < b⁻¹ ↔ b < a⁻¹ := +have (a⁻¹)⁻¹ < b⁻¹ ↔ b < a⁻¹, from inv_lt_inv_iff, +by rwa inv_inv at this + +@[to_additive] +lemma le_inv_mul_iff_mul_le : b ≤ a⁻¹ * c ↔ a * b ≤ c := +have a⁻¹ * (a * b) ≤ a⁻¹ * c ↔ a * b ≤ c, from mul_le_mul_iff_left _, +by rwa inv_mul_cancel_left at this + +@[simp, to_additive] +lemma inv_mul_le_iff_le_mul : b⁻¹ * a ≤ c ↔ a ≤ b * c := +have b⁻¹ * a ≤ b⁻¹ * (b * c) ↔ a ≤ b * c, from mul_le_mul_iff_left _, +by rwa inv_mul_cancel_left at this + +@[to_additive] +lemma mul_inv_le_iff_le_mul : a * c⁻¹ ≤ b ↔ a ≤ b * c := +by rw [mul_comm a, mul_comm b, inv_mul_le_iff_le_mul] + +@[simp, to_additive] +lemma mul_inv_le_iff_le_mul' : a * b⁻¹ ≤ c ↔ a ≤ b * c := +by rw [← inv_mul_le_iff_le_mul, mul_comm] + +@[to_additive] +lemma inv_mul_le_iff_le_mul' : c⁻¹ * a ≤ b ↔ a ≤ b * c := +by rw [inv_mul_le_iff_le_mul, mul_comm] + +@[simp, to_additive] +lemma lt_inv_mul_iff_mul_lt : b < a⁻¹ * c ↔ a * b < c := +have a⁻¹ * (a * b) < a⁻¹ * c ↔ a * b < c, from mul_lt_mul_iff_left _, +by rwa inv_mul_cancel_left at this + +@[simp, to_additive] +lemma inv_mul_lt_iff_lt_mul : b⁻¹ * a < c ↔ a < b * c := +have b⁻¹ * a < b⁻¹ * (b * c) ↔ a < b * c, from mul_lt_mul_iff_left _, +by rwa inv_mul_cancel_left at this + +@[to_additive] +lemma inv_mul_lt_iff_lt_mul_right : c⁻¹ * a < b ↔ a < b * c := +by rw [inv_mul_lt_iff_lt_mul, mul_comm] + +end ordered_comm_group + +section ordered_add_comm_group +variables [ordered_add_comm_group α] {a b c d : α} + lemma sub_nonneg_of_le (h : b ≤ a) : 0 ≤ a - b := begin have h := add_le_add_right h (-b), @@ -834,18 +1218,6 @@ begin rwa [sub_add_cancel, zero_add] at h end -lemma add_le_of_le_neg_add (h : b ≤ -a + c) : a + b ≤ c := -begin - have h := add_le_add_left h a, - rwa add_neg_cancel_left at h -end - -lemma le_neg_add_of_add_le (h : a + b ≤ c) : b ≤ -a + c := -begin - have h := add_le_add_left h (-a), - rwa neg_add_cancel_left at h -end - lemma add_le_of_le_sub_left (h : b ≤ c - a) : a + b ≤ c := begin have h := add_le_add_left h a, @@ -870,18 +1242,6 @@ begin rwa add_neg_cancel_right at h end -lemma le_add_of_neg_add_le (h : -b + a ≤ c) : a ≤ b + c := -begin - have h := add_le_add_left h b, - rwa add_neg_cancel_left at h -end - -lemma neg_add_le_of_le_add (h : a ≤ b + c) : -b + a ≤ c := -begin - have h := add_le_add_left h (-b), - rwa neg_add_cancel_left at h -end - lemma le_add_of_sub_left_le (h : a - b ≤ c) : a ≤ b + c := begin have h := add_le_add_right h b, @@ -906,30 +1266,6 @@ begin rwa add_neg_cancel_right at h end -lemma le_add_of_neg_add_le_left (h : -b + a ≤ c) : a ≤ b + c := -begin - rw add_comm at h, - exact le_add_of_sub_left_le h -end - -lemma neg_add_le_left_of_le_add (h : a ≤ b + c) : -b + a ≤ c := -begin - rw add_comm, - exact sub_left_le_of_le_add h -end - -lemma le_add_of_neg_add_le_right (h : -c + a ≤ b) : a ≤ b + c := -begin - rw add_comm at h, - exact le_add_of_sub_right_le h -end - -lemma neg_add_le_right_of_le_add (h : a ≤ b + c) : -c + a ≤ b := -begin - rw add_comm at h, - apply neg_add_le_left_of_le_add h -end - lemma le_add_of_neg_le_sub_left (h : -a ≤ b - c) : c ≤ a + b := le_add_of_neg_add_le_left (add_le_of_le_sub_right h) @@ -957,18 +1293,6 @@ add_le_add_right h (-c) lemma sub_le_sub (hab : a ≤ b) (hcd : c ≤ d) : a - d ≤ b - c := add_le_add hab (neg_le_neg hcd) -lemma add_lt_of_lt_neg_add (h : b < -a + c) : a + b < c := -begin - have h := add_lt_add_left h a, - rwa add_neg_cancel_left at h -end - -lemma lt_neg_add_of_add_lt (h : a + b < c) : b < -a + c := -begin - have h := add_lt_add_left h (-a), - rwa neg_add_cancel_left at h -end - lemma add_lt_of_lt_sub_left (h : b < c - a) : a + b < c := begin have h := add_lt_add_left h a, @@ -993,18 +1317,6 @@ begin rwa add_neg_cancel_right at h end -lemma lt_add_of_neg_add_lt (h : -b + a < c) : a < b + c := -begin - have h := add_lt_add_left h b, - rwa add_neg_cancel_left at h -end - -lemma neg_add_lt_of_lt_add (h : a < b + c) : -b + a < c := -begin - have h := add_lt_add_left h (-b), - rwa neg_add_cancel_left at h -end - lemma lt_add_of_sub_left_lt (h : a - b < c) : a < b + c := begin have h := add_lt_add_right h b, @@ -1029,30 +1341,6 @@ begin rwa add_neg_cancel_right at h end -lemma lt_add_of_neg_add_lt_left (h : -b + a < c) : a < b + c := -begin - rw add_comm at h, - exact lt_add_of_sub_left_lt h -end - -lemma neg_add_lt_left_of_lt_add (h : a < b + c) : -b + a < c := -begin - rw add_comm, - exact sub_left_lt_of_lt_add h -end - -lemma lt_add_of_neg_add_lt_right (h : -c + a < b) : a < b + c := -begin - rw add_comm at h, - exact lt_add_of_sub_right_lt h -end - -lemma neg_add_lt_right_of_lt_add (h : a < b + c) : -c + a < b := -begin - rw add_comm at h, - apply neg_add_lt_left_of_lt_add h -end - lemma lt_add_of_neg_lt_sub_left (h : -a < b - c) : c < a + b := lt_add_of_neg_add_lt_left (add_lt_of_lt_sub_right h) @@ -1098,71 +1386,6 @@ calc ... < a + 0 : add_lt_add_left (neg_neg_of_pos h) _ ... = a : by rw add_zero -lemma add_le_add_three {a b c d e f : α} (h₁ : a ≤ d) (h₂ : b ≤ e) (h₃ : c ≤ f) : - a + b + c ≤ d + e + f := -begin - apply le_trans, - apply add_le_add, - apply add_le_add, - assumption', - apply le_refl -end - -@[simp] lemma neg_neg_iff_pos : -a < 0 ↔ 0 < a := -⟨ pos_of_neg_neg, neg_neg_of_pos ⟩ - -@[simp] lemma neg_le_neg_iff : -a ≤ -b ↔ b ≤ a := -have a + b - a ≤ a + b - b ↔ -a ≤ -b, from add_le_add_iff_left _, -by simp at this; simp [this] - -lemma neg_le : -a ≤ b ↔ -b ≤ a := -have -a ≤ -(-b) ↔ -b ≤ a, from neg_le_neg_iff, -by rwa neg_neg at this - -lemma le_neg : a ≤ -b ↔ b ≤ -a := -have -(-a) ≤ -b ↔ b ≤ -a, from neg_le_neg_iff, -by rwa neg_neg at this - -lemma neg_le_iff_add_nonneg : -a ≤ b ↔ 0 ≤ a + b := -(add_le_add_iff_left a).symm.trans $ by rw add_neg_self - -lemma le_neg_iff_add_nonpos : a ≤ -b ↔ a + b ≤ 0 := -(add_le_add_iff_right b).symm.trans $ by rw neg_add_self - -@[simp] lemma neg_nonpos : -a ≤ 0 ↔ 0 ≤ a := -have -a ≤ -0 ↔ 0 ≤ a, from neg_le_neg_iff, -by rwa neg_zero at this - -@[simp] lemma neg_nonneg : 0 ≤ -a ↔ a ≤ 0 := -have -0 ≤ -a ↔ a ≤ 0, from neg_le_neg_iff, -by rwa neg_zero at this - -lemma neg_le_self (h : 0 ≤ a) : -a ≤ a := -le_trans (neg_nonpos.2 h) h - -lemma self_le_neg (h : a ≤ 0) : a ≤ -a := -le_trans h (neg_nonneg.2 h) - -@[simp] lemma neg_lt_neg_iff : -a < -b ↔ b < a := -have a + b - a < a + b - b ↔ -a < -b, from add_lt_add_iff_left _, -by simp at this; simp [this] - -lemma neg_lt_zero : -a < 0 ↔ 0 < a := -have -a < -0 ↔ 0 < a, from neg_lt_neg_iff, -by rwa neg_zero at this - -lemma neg_pos : 0 < -a ↔ a < 0 := -have -0 < -a ↔ a < 0, from neg_lt_neg_iff, -by rwa neg_zero at this - -lemma neg_lt : -a < b ↔ -b < a := -have -a < -(-b) ↔ -b < a, from neg_lt_neg_iff, -by rwa neg_neg at this - -lemma lt_neg : a < -b ↔ b < -a := -have -(-a) < -b ↔ b < -a, from neg_lt_neg_iff, -by rwa neg_neg at this - @[simp] lemma sub_le_sub_iff_left (a : α) {b c : α} : a - b ≤ a - c ↔ c ≤ b := (add_le_add_iff_left _).trans neg_le_neg_iff @@ -1195,35 +1418,18 @@ by rwa sub_self at this have a - b < b - b ↔ a < b, from sub_lt_sub_iff_right b, by rwa sub_self at this -lemma le_neg_add_iff_add_le : b ≤ -a + c ↔ a + b ≤ c := -have -a + (a + b) ≤ -a + c ↔ a + b ≤ c, from add_le_add_iff_left _, -by rwa neg_add_cancel_left at this - lemma le_sub_iff_add_le' : b ≤ c - a ↔ a + b ≤ c := by rw [sub_eq_add_neg, add_comm, le_neg_add_iff_add_le] lemma le_sub_iff_add_le : a ≤ c - b ↔ a + b ≤ c := by rw [le_sub_iff_add_le', add_comm] -@[simp] lemma neg_add_le_iff_le_add : -b + a ≤ c ↔ a ≤ b + c := -have -b + a ≤ -b + (b + c) ↔ a ≤ b + c, from add_le_add_iff_left _, -by rwa neg_add_cancel_left at this - lemma sub_le_iff_le_add' : a - b ≤ c ↔ a ≤ b + c := by rw [sub_eq_add_neg, add_comm, neg_add_le_iff_le_add] lemma sub_le_iff_le_add : a - c ≤ b ↔ a ≤ b + c := by rw [sub_le_iff_le_add', add_comm] -lemma add_neg_le_iff_le_add : a + -c ≤ b ↔ a ≤ b + c := -sub_le_iff_le_add - -@[simp] lemma add_neg_le_iff_le_add' : a + -b ≤ c ↔ a ≤ b + c := -sub_le_iff_le_add' - -lemma neg_add_le_iff_le_add' : -c + a ≤ b ↔ a ≤ b + c := -by rw [neg_add_le_iff_le_add, add_comm] - @[simp] lemma neg_le_sub_iff_le_add : -b ≤ a - c ↔ c ≤ a + b := le_sub_iff_add_le.trans neg_add_le_iff_le_add' @@ -1236,29 +1442,18 @@ sub_le_iff_le_add'.trans sub_le_iff_le_add.symm theorem le_sub : a ≤ b - c ↔ c ≤ b - a := le_sub_iff_add_le'.trans le_sub_iff_add_le.symm -@[simp] lemma lt_neg_add_iff_add_lt : b < -a + c ↔ a + b < c := -have -a + (a + b) < -a + c ↔ a + b < c, from add_lt_add_iff_left _, -by rwa neg_add_cancel_left at this - lemma lt_sub_iff_add_lt' : b < c - a ↔ a + b < c := by rw [sub_eq_add_neg, add_comm, lt_neg_add_iff_add_lt] lemma lt_sub_iff_add_lt : a < c - b ↔ a + b < c := by rw [lt_sub_iff_add_lt', add_comm] -@[simp] lemma neg_add_lt_iff_lt_add : -b + a < c ↔ a < b + c := -have -b + a < -b + (b + c) ↔ a < b + c, from add_lt_add_iff_left _, -by rwa neg_add_cancel_left at this - lemma sub_lt_iff_lt_add' : a - b < c ↔ a < b + c := by rw [sub_eq_add_neg, add_comm, neg_add_lt_iff_lt_add] lemma sub_lt_iff_lt_add : a - c < b ↔ a < b + c := by rw [sub_lt_iff_lt_add', add_comm] -lemma neg_add_lt_iff_lt_add_right : -c + a < b ↔ a < b + c := -by rw [neg_add_lt_iff_lt_add, add_comm] - @[simp] lemma neg_lt_sub_iff_lt_add : -b < a - c ↔ c < a + b := lt_sub_iff_add_lt.trans neg_add_lt_iff_lt_add_right @@ -1279,17 +1474,27 @@ sub_lt_iff_lt_add'.trans (lt_add_iff_pos_left _) end ordered_add_comm_group -/-- -The `add_lt_add_left` field of `ordered_add_comm_group` is redundant, but it is in core so -we can't remove it for now. This alternative constructor is the best we can do. +/- +TODO: +The `add_lt_add_left` field of `ordered_add_comm_group` is redundant, +and it is no longer in core so we can remove it now. +This alternative constructor is a workaround until someone fixes this. -/ -def ordered_add_comm_group.mk' {α : Type u} [add_comm_group α] [partial_order α] - (add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b) : - ordered_add_comm_group α := -{ add_le_add_left := add_le_add_left, - ..(by apply_instance : add_comm_group α), - ..(by apply_instance : partial_order α) } +/-- Alternative constructor for ordered commutative groups, +that avoids the field `mul_lt_mul_left`. -/ +@[to_additive "Alternative constructor for ordered commutative groups, +that avoids the field `mul_lt_mul_left`."] +def ordered_comm_group.mk' {α : Type u} [comm_group α] [partial_order α] + (mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b) : + ordered_comm_group α := +{ mul_le_mul_left := mul_le_mul_left, + ..(by apply_instance : comm_group α), + ..(by apply_instance : partial_order α) } + +/-- A decidable linearly ordered cancellative additive commutative monoid +is an additive commutative monoid with a decidable linear order +in which addition is cancellative and strictly monotone. -/ @[protect_proj] class decidable_linear_ordered_cancel_add_comm_monoid (α : Type u) extends ordered_cancel_add_comm_monoid α, decidable_linear_order α @@ -1326,6 +1531,9 @@ begin rw [add_comm a c, add_comm b c, add_comm _ c], apply max_add_add_left end end decidable_linear_ordered_cancel_add_comm_monoid +/-- A decidable linearly ordered additive commutative group is an +additive commutative group with a decidable linear order in which +addition is strictly monotone. -/ @[protect_proj] class decidable_linear_ordered_add_comm_group (α : Type u) extends add_comm_group α, decidable_linear_order α := (add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b) @@ -1369,6 +1577,7 @@ by rw [min_eq_neg_max_neg_neg, neg_neg, neg_neg] lemma max_eq_neg_min_neg_neg (a b : α) : max a b = - min (-a) (-b) := by rw [min_neg_neg, neg_neg] +/-- `abs a` is the absolute value of `a`. -/ def abs (a : α) : α := max a (-a) lemma abs_of_nonneg {a : α} (h : 0 ≤ a) : abs a = a := @@ -1533,7 +1742,7 @@ begin apply le_refl end -lemma dist_bdd_within_interval {a b lb ub : α} (h : lb < ub) (hal : lb ≤ a) (hau : a ≤ ub) +lemma dist_bdd_within_interval {a b lb ub : α} (hal : lb ≤ a) (hau : a ≤ ub) (hbl : lb ≤ b) (hbu : b ≤ ub) : abs (a - b) ≤ ub - lb := begin cases (decidable.em (b ≤ a)) with hba hba,