feat: add some missing convenience lemmas about ordered modules

Author: j-loreaux

Mathlib/Algebra/Order/Module/Defs.lean

@@ -566,6 +566,22 @@ lemma pos_of_smul_pos_left [PosSMulReflectLT α β] (h : 0 < a • b) (ha : 0 
 lemma neg_of_smul_neg_left [PosSMulReflectLT α β] (h : a • b < 0) (ha : 0 ≤ a) : b < 0 :=
   lt_of_smul_lt_smul_left (by rwa [smul_zero]) ha
 
+lemma nonneg_of_smul_nonneg_of_pos_left [PosSMulReflectLE α β] (h : 0 ≤ a • b) (ha : 0 < a) :
+    0 ≤ b :=
+  le_of_smul_le_smul_of_pos_left (by simpa) ha
+
+lemma nonpos_of_smul_nonpos_of_pos_left [PosSMulReflectLE α β] (h : a • b ≤ 0) (ha : 0 < a) :
+    b ≤ 0 :=
+  le_of_smul_le_smul_of_pos_left (by simpa) ha
+
+lemma smul_nonneg_iff_nonneg_of_pos_left [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) :
+    0 ≤ a • b ↔ 0 ≤ b :=
+  ⟨(nonneg_of_smul_nonneg_of_pos_left · ha), smul_nonneg ha.le⟩
+
+lemma smul_nonpos_iff_nonpos_of_pos_left [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) :
+    a • b ≤ 0 ↔ b ≤ 0 :=
+  ⟨(nonpos_of_smul_nonpos_of_pos_left · ha), smul_nonpos_of_nonneg_of_nonpos ha.le⟩
+
 end Preorder
 end SMulZeroClass
 
@@ -602,6 +618,22 @@ lemma pos_iff_pos_of_smul_pos [PosSMulReflectLT α β] [SMulPosReflectLT α β]
     0 < a ↔ 0 < b :=
   ⟨pos_of_smul_pos_left hab ∘ le_of_lt, pos_of_smul_pos_right hab ∘ le_of_lt⟩
 
+lemma nonneg_of_smul_nonneg_of_pos_right [SMulPosReflectLE α β] (h : 0 ≤ a • b) (hb : 0 < b) :
+    0 ≤ a :=
+  le_of_smul_le_smul_of_pos_right (by simpa) hb
+
+lemma nonpos_of_smul_nonpos_of_pos_right [SMulPosReflectLE α β] (h : a • b ≤ 0) (hb : 0 < b) :
+    a ≤ 0 :=
+  le_of_smul_le_smul_of_pos_right (by simpa) hb
+
+lemma smul_nonneg_iff_nonneg_of_pos_right [SMulPosMono α β] [SMulPosReflectLE α β] (hb : 0 < b) :
+    0 ≤ a • b ↔ 0 ≤ a :=
+  ⟨(nonneg_of_smul_nonneg_of_pos_right · hb), (smul_nonneg' · hb.le)⟩
+
+lemma smul_nonpos_iff_nonpos_of_pos_right [SMulPosMono α β] [SMulPosReflectLE α β] (hb : 0 < b) :
+    a • b ≤ 0 ↔ a ≤ 0 :=
+  ⟨(nonpos_of_smul_nonpos_of_pos_right · hb), (smul_nonpos_of_nonpos_of_nonneg · hb.le)⟩
+
 lemma IsOrderedModule.of_smul_one_mono
     [MulOneClass β] [PosMulMono β] [MulPosMono β] [IsScalarTower α β β]
     (h : Monotone (fun x : α ↦ x • (1 : β))) : IsOrderedModule α β where