From b87562719814447e77c17ff03492f7c11573f475 Mon Sep 17 00:00:00 2001
From: Lars - he/him <l.b.vandenhaak@gmail.com>
Date: Thu, 12 Sep 2024 13:26:20 +0200
Subject: [PATCH] feat: add ediv_nonneg_of_nonpos_of_nonpos to DivModLemmas
 (#5320)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The theorem

```lean
namespace Int

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]
    have le_succ {a: Int} : a ≤ a+1 := (le_add_one (Int.le_refl a))
    have h2: 0 ≤ ((↑b:Int) + 1) := Int.le_trans (ofNat_zero_le b) le_succ
    have h3: (0:Int) ≤ ↑a / (↑b + 1) := (ediv_nonneg (ofNat_zero_le a) h2)
    exact Int.le_trans h3 le_succ
```
is nontrivial to prove from existing theorems and would be nice to add
as standard theorem in DivModLemmas.

See the zullip conversation
[here](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Adding.20theorem.20theorem.20ediv_nonneg'.20for.20negative.20a.20and.20b)

---------

Co-authored-by: Kim Morrison <kim@tqft.net>
---
 src/Init/Data/Int/DivModLemmas.lean | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean
index 53a4ff2ae7..123d8f3124 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)