feat(algebra/order/ring/defs): negative versions of order lemmas (#18831)

eric-wieser · eric-wieser · commit 44e29dbcff83 · 2023-04-20T11:35:11.000Z
For each of a handful of lemmas with a `0 &lt;` or `0 ≤` assumption, this adds a variant with a `&lt; 0` or `≤ 0` assumption.
diff --git a/src/algebra/order/field/basic.lean b/src/algebra/order/field/basic.lean
@@ -595,6 +595,9 @@ lt_iff_lt_of_le_iff_le $ div_le_iff_of_neg hc
 lemma lt_div_iff_of_neg' (hc : c < 0) : a < b / c ↔ b < c * a :=
 by rw [mul_comm, lt_div_iff_of_neg hc]
 
+lemma div_le_one_of_ge (h : b ≤ a) (hb : b ≤ 0) : a / b ≤ 1 :=
+by simpa only [neg_div_neg_eq] using div_le_one_of_le (neg_le_neg h) (neg_nonneg_of_nonpos hb)
+
 /-! ### Bi-implications of inequalities using inversions -/
 
 lemma inv_le_inv_of_neg (ha : a < 0) (hb : b < 0) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a :=
diff --git a/src/algebra/order/ring/defs.lean b/src/algebra/order/ring/defs.lean
@@ -327,6 +327,22 @@ lemma mul_le_mul_of_nonpos_of_nonpos' (hca : c ≤ a) (hdb : d ≤ b) (ha : a 
   a * b ≤ c * d :=
 (mul_le_mul_of_nonpos_left hdb ha).trans $ mul_le_mul_of_nonpos_right hca hd
 
+/-- Variant of `mul_le_of_le_one_left` for `b` non-positive instead of non-negative.  -/
+lemma le_mul_of_le_one_left (hb : b ≤ 0) (h : a ≤ 1) : b ≤ a * b :=
+by simpa only [one_mul] using mul_le_mul_of_nonpos_right h hb
+
+/-- Variant of `le_mul_of_one_le_left` for `b` non-positive instead of non-negative. -/
+lemma mul_le_of_one_le_left (hb : b ≤ 0) (h : 1 ≤ a) : a * b ≤ b :=
+by simpa only [one_mul] using mul_le_mul_of_nonpos_right h hb
+
+/-- Variant of `mul_le_of_le_one_right` for `a` non-positive instead of non-negative. -/
+lemma le_mul_of_le_one_right (ha : a ≤ 0) (h : b ≤ 1) : a ≤ a * b :=
+by simpa only [mul_one] using mul_le_mul_of_nonpos_left h ha
+
+/-- Variant of `le_mul_of_one_le_right` for `a` non-positive instead of non-negative. -/
+lemma mul_le_of_one_le_right (ha : a ≤ 0) (h : 1 ≤ b) : a * b ≤ a :=
+by simpa only [mul_one] using mul_le_mul_of_nonpos_left h ha
+
 section monotone
 variables [preorder β] {f g : β → α}
 
@@ -568,6 +584,22 @@ by simpa only [mul_neg, neg_lt_neg_iff] using mul_lt_mul_of_pos_right h (neg_pos
 lemma mul_pos_of_neg_of_neg {a b : α} (ha : a < 0) (hb : b < 0) : 0 < a * b :=
 by simpa only [zero_mul] using mul_lt_mul_of_neg_right ha hb
 
+/-- Variant of `mul_lt_of_lt_one_left` for `b` negative instead of positive. -/
+lemma lt_mul_of_lt_one_left (hb : b < 0) (h : a < 1) : b < a * b :=
+by simpa only [one_mul] using mul_lt_mul_of_neg_right h hb
+
+/-- Variant of `lt_mul_of_one_lt_left` for `b` negative instead of positive. -/
+lemma mul_lt_of_one_lt_left (hb : b < 0) (h : 1 < a) : a * b < b :=
+by simpa only [one_mul] using mul_lt_mul_of_neg_right h hb
+
+/-- Variant of `mul_lt_of_lt_one_right` for `a` negative instead of positive. -/
+lemma lt_mul_of_lt_one_right (ha : a < 0) (h : b < 1) : a < a * b :=
+by simpa only [mul_one] using mul_lt_mul_of_neg_left h ha
+
+/-- Variant of `lt_mul_of_lt_one_right` for `a` negative instead of positive. -/
+lemma mul_lt_of_one_lt_right (ha : a < 0) (h : 1 < b) : a * b < a :=
+by simpa only [mul_one] using mul_lt_mul_of_neg_left h ha
+
 section monotone
 variables [preorder β] {f g : β → α}
 
diff --git a/src/algebra/order/ring/lemmas.lean b/src/algebra/order/ring/lemmas.lean
@@ -548,7 +548,10 @@ lemma mul_lt_iff_lt_one_left
   a * b < b ↔ a < 1 :=
 iff.trans (by rw [one_mul]) (mul_lt_mul_right b0)
 
-/-! Lemmas of the form `1 ≤ b → a ≤ a * b`. -/
+/-! Lemmas of the form `1 ≤ b → a ≤ a * b`.
+
+Variants with `< 0` and `≤ 0` instead of `0 <` and `0 ≤` appear in `algebra/order/ring/defs` (which
+imports this file) as they need additional results which are not yet available here. -/
 
 lemma mul_le_of_le_one_left [mul_pos_mono α] (hb : 0 ≤ b) (h : a ≤ 1) : a * b ≤ b :=
 by simpa only [one_mul] using mul_le_mul_of_nonneg_right h hb
