feat(algebra/order/field): prove a / a ≤ 1 (#11118)

src/algebra/order/field.lean

@@ -166,6 +166,9 @@ by rw [mul_comm, inv_mul_le_iff h]
 lemma mul_inv_le_iff' (h : 0 < b) : a * b⁻¹ ≤ c ↔ a ≤ c * b :=
 by rw [mul_comm, inv_mul_le_iff' h]
 
+lemma div_self_le_one (a : α) : a / a ≤ 1 :=
+if h : a = 0 then by simp [h] else by simp [h]
+
 lemma inv_mul_lt_iff (h : 0 < b) : b⁻¹ * a < c ↔ a < b * c :=
 begin
   rw [inv_eq_one_div, mul_comm, ← div_eq_mul_one_div],

src/data/real/nnreal.lean

@@ -549,8 +549,7 @@ by simpa only [div_eq_mul_inv] using mul_pos hr (inv_pos.2 hp)
 
 protected lemma mul_inv {r p : ℝ≥0} : (r * p)⁻¹ = p⁻¹ * r⁻¹ := nnreal.eq $ mul_inv_rev₀ _ _
 
-lemma div_self_le (r : ℝ≥0) : r / r ≤ 1 :=
-if h : r = 0 then by simp [h] else by rw [div_self h]
+lemma div_self_le (r : ℝ≥0) : r / r ≤ 1 := div_self_le_one (r : ℝ)
 
 @[simp] lemma inv_le {r p : ℝ≥0} (h : r ≠ 0) : r⁻¹ ≤ p ↔ 1 ≤ r * p :=
 by rw [← mul_le_mul_left (pos_iff_ne_zero.2 h), mul_inv_cancel h]