diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean
index 53a4ff2ae7c0..123d8f312448 100644
--- a/src/Init/Data/Int/DivModLemmas.lean
+++ b/src/Init/Data/Int/DivModLemmas.lean
@@ -306,6 +306,22 @@ theorem ediv_nonneg {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a / b :=
   match a, b, eq_ofNat_of_zero_le Ha, eq_ofNat_of_zero_le Hb with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => ofNat_zero_le _
 
+theorem ediv_nonneg_of_nonpos_of_nonpos {a b : Int} (Ha : a ≤ 0) (Hb : b ≤ 0) : 0 ≤ a / b := by
+  match a, b with
+  | ofNat a, b =>
+    match Int.le_antisymm Ha (ofNat_zero_le a) with
+    | h1 =>
+      rw [h1, zero_ediv]
+      exact Int.le_refl 0
+  | a, ofNat b =>
+    match Int.le_antisymm Hb (ofNat_zero_le  b) with
+    | h1 =>
+      rw [h1, Int.ediv_zero]
+      exact Int.le_refl 0
+  | negSucc a, negSucc b =>
+    rw [Int.div_def, ediv]
+    exact le_add_one (ediv_nonneg (ofNat_zero_le a) (Int.le_trans (ofNat_zero_le b) (le.intro 1 rfl)))
+
 theorem ediv_nonpos {a b : Int} (Ha : 0 ≤ a) (Hb : b ≤ 0) : a / b ≤ 0 :=
   Int.nonpos_of_neg_nonneg <| Int.ediv_neg .. ▸ Int.ediv_nonneg Ha (Int.neg_nonneg_of_nonpos Hb)