Commit 2022-05-12 20:54 3c1ced3b
View on Github →feat(data/nat/basic): four lemmas on nat and int division (#13991)
lt_div_iff_mul_lt (hnd : d ∣ n) : a < n / d ↔ d * a < n
div_left_inj (hda : d ∣ a) (hdb : d ∣ b) : a / d = b / d ↔ a = b (for ℕ and ℤ)
div_lt_div_of_lt_of_dvd (hdb : d ∣ b) (h : a < b) : a / d < b / d