div_le_div

Stream: Is there code for X?

[Benjamin Davidson]

Do we not have the following lemmas? I wasn't able to find them.

import algebra.ordered_field

lemma div_le_div_new {α : Type*} [linear_ordered_field α] {a b c : α}
  (ha : 0 ≤ a) (hc : 0 < c) (h : c ≤ b) :
  a / b ≤ a / c :=
(div_le_div_iff (hc.trans_le h) hc).mpr $ mul_le_mul_of_nonneg_left h ha

lemma div_le_div_new' {α : Type*} [ordered_comm_group α] (a : α) {b c : α} (h : c ≤ b) :
  a * b⁻¹ ≤ a * c⁻¹ :=
div_le_div_iff'.mpr $ mul_le_mul_left' h a

lemma div_le_new {α : Type*} [linear_ordered_field α] {a b : α}
  (ha : 0 ≤ a) (hb : 1 ≤ b) :
  a / b ≤ a :=
by simpa only [div_one] using div_le_div_new ha zero_lt_one hb

lemma div_le_new' {α : Type*} [ordered_comm_group α] (a : α) {b : α} (h : 1 ≤ b) :
  a * b⁻¹ ≤ a :=
by rwa [mul_inv_le_iff_le_mul', le_mul_iff_one_le_left']