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 <[email protected]>

Author: b-mehta

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`.