0 ≤ b → ((a / b : ℤ) : ℚ) ≤ (a / b : ℚ)

Stream: Is there code for X?

[Scott Morrison]

example (a b : ℤ) (w : 0 ≤ b) : ((a / b : ℤ) : ℚ) ≤ (a / b : ℚ) := sorry

Location in library / proof / name?

(slim_check agrees there are no counterexamples due to misunderstanding rounding!)

[Yury G. Kudryashov]

import Mathlib.Data.Rat.Order
import Mathlib.Algebra.Order.Field.Basic

example (a b : ℤ) (w : 0 ≤ b) : ((a / b : ℤ) : ℚ) ≤ (a / b : ℚ) := by
  rcases w.eq_or_lt with rfl | hb;
  · simp [Int.ediv_zero]
  · rw [le_div_iff (Int.cast_pos.2 hb)]
    norm_cast
    exact Int.ediv_mul_le _ hb.ne'

About location: #find_home?

[Yury G. Kudryashov]

If we move lemmas about Rat to Std, then you may need a version of le_div_iff.

[Yaël Dillies]

algebra.order.floor

[Yaël Dillies]

Your lemma is basically docs3#int.floor_le

[Ruben Van de Velde]

Looking at the code, docs#Int.floor_le might be more useful, but I don't see anything similar to docs#Nat.floor_div_eq_div for Int on first sight