From aeddc0d22ef2ca248c4aa059a3bd8d260f571119 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 25 Nov 2025 15:04:39 +0000 Subject: [PATCH] feat: add lemmas for `a / c < b / c` on `Int` (#11327) This PR adds two lemmas to prove `a / c < b / c`. --------- Co-authored-by: Markus Himmel --- src/Init/Data/Int/DivMod/Lemmas.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/Init/Data/Int/DivMod/Lemmas.lean b/src/Init/Data/Int/DivMod/Lemmas.lean index 0f803ec827..bfdfdff437 100644 --- a/src/Init/Data/Int/DivMod/Lemmas.lean +++ b/src/Init/Data/Int/DivMod/Lemmas.lean @@ -1781,6 +1781,16 @@ theorem ediv_lt_ediv_iff_of_dvd_of_neg_of_neg {a b c d : Int} (hb : b < 0) (hd : obtain ⟨⟨x, rfl⟩, y, rfl⟩ := hba, hdc simp [*, Int.ne_of_lt, d.mul_assoc, b.mul_comm] +theorem ediv_lt_ediv_of_lt {a b c : Int} (h : a < b) (hcb : c ∣ b) (hc : 0 < c) : + a / c < b / c := + Int.lt_ediv_of_mul_lt (Int.le_of_lt hc) hcb + (Int.lt_of_le_of_lt (Int.ediv_mul_le _ (Int.ne_of_gt hc)) h) + +theorem ediv_lt_ediv_of_lt_of_neg {a b c : Int} (h : b < a) (hca : c ∣ a) (hc : c < 0) : + a / c < b / c := + (Int.ediv_lt_iff_of_dvd_of_neg hc hca).2 + (Int.lt_of_le_of_lt (Int.mul_ediv_self_le (Int.ne_of_lt hc)) h) + /-! ### `tdiv` and ordering -/ -- Theorems about `tdiv` and ordering, whose `ediv` analogues are in `Bootstrap.lean`.