[Merged by Bors] - feat(data/nnreal): filling out some lemmas

src/data/real/nnreal.lean

@@ -596,9 +596,27 @@ by rw [div_eq_inv_mul, ← mul_le_iff_le_inv hr, mul_comm]
 lemma div_le_iff {a b r : ℝ≥0} (hr : r ≠ 0) : a / r ≤ b ↔ a ≤ b * r :=
 @div_le_iff ℝ _ a r b $ pos_iff_ne_zero.2 hr
 
+lemma div_le_iff' {a b r : ℝ≥0} (hr : r ≠ 0) : a / r ≤ b ↔ a ≤ r * b :=
+@div_le_iff' ℝ _ a r b $ pos_iff_ne_zero.2 hr
+
+lemma le_div_iff {a b r : ℝ≥0} (hr : r ≠ 0) : a ≤ b / r ↔ a * r ≤ b :=
+@le_div_iff ℝ _ a b r $ pos_iff_ne_zero.2 hr
+
+lemma le_div_iff' {a b r : ℝ≥0} (hr : r ≠ 0) : a ≤ b / r ↔ r * a ≤ b :=
+@le_div_iff' ℝ _ a b r $ pos_iff_ne_zero.2 hr
+
+lemma div_lt_iff {a b r : ℝ≥0} (hr : r ≠ 0) : a / r < b ↔ a < b * r :=
+lt_iff_lt_of_le_iff_le (le_div_iff hr)
+
+lemma div_lt_iff' {a b r : ℝ≥0} (hr : r ≠ 0) : a / r < b ↔ a < r * b :=
+lt_iff_lt_of_le_iff_le (le_div_iff' hr)
+
 lemma lt_div_iff {a b r : ℝ≥0} (hr : r ≠ 0) : a < b / r ↔ a * r < b :=
 lt_iff_lt_of_le_iff_le (div_le_iff hr)
 
+lemma lt_div_iff' {a b r : ℝ≥0} (hr : r ≠ 0) : a < b / r ↔ r * a < b :=
+lt_iff_lt_of_le_iff_le (div_le_iff' hr)
+
 lemma mul_lt_of_lt_div {a b r : ℝ≥0} (h : a < b / r) : a * r < b :=
 begin
   refine (lt_div_iff $ λ hr, false.elim _).1 h,
@@ -643,9 +661,6 @@ half_lt_self (bot_lt_iff_ne_bot.2 h)
 lemma two_inv_lt_one : (2⁻¹:ℝ≥0) < 1 :=
 by simpa using half_lt_self zero_ne_one.symm
 
-lemma div_lt_iff {a b c : ℝ≥0} (hc : c ≠ 0) : b / c < a ↔ b < a * c :=
-lt_iff_lt_of_le_iff_le $ nnreal.le_div_iff_mul_le hc
-
 lemma div_lt_one_of_lt {a b : ℝ≥0} (h : a < b) : a / b < 1 :=
 begin
   rwa [div_lt_iff, one_mul],