Adding theorem theorem ediv_nonneg' for negative a and b

Stream: general

[Lars]

So I was trying to proof this property:
theorem ediv_nonneg' {a b : Int} (Ha : a ≤ 0) (Hb : b ≤ 0) : 0 ≤ a / b

which is almost the same as: Int.ediv_nonneg, but now using negative a and b.

However the proof was non-trivial for me, as a newer user. Would it make sense to add this to the standard library? (same place as ediv_nonneg) I was actually expecting it to be there. If yes, I can make a pull request. This was my proof. (could probably be cleaner)

theorem ediv_nonneg' {a b : Int} (Ha : a ≤ 0) (Hb : b ≤ 0) : 0 ≤ a / b := by
  match a, b with
  | Int.ofNat a, b =>
    match Int.le_antisymm_iff.mpr ⟨Ha, Int.zero_le_ofNat a⟩ with
    | h1 =>
    rw [h1, Int.zero_ediv]
  | a, Int.ofNat b =>
    match Int.le_antisymm_iff.mpr ⟨Hb, Int.zero_le_ofNat b⟩ with
    | h1 =>
    rw [h1, Int.ediv_zero]
  | Int.negSucc a, Int.negSucc b =>
    rw [Int.div_def, Int.ediv]
    have le_succ {a: Int} : a ≤ a+1 := (Int.le_add_one (Int.le_refl a))
    have h2: 0 ≤ ((↑b:Int) + 1) := Int.le_trans (Int.ofNat_zero_le b) le_succ
    have h3: (0:Int) ≤ ↑a / (↑b + 1) := (Int.ediv_nonneg (Int.ofNat_zero_le a) h2)
    exact Int.le_trans h3 le_succ

[Kim Morrison]

This does appear to be missing, and I agree it's nontrivial to prove from existing lemmas. Your proof requires Mathlib imports, however. I'd be happy to have a PR for this. Let's rename to ediv_nonneg_of_nonpos_of_nonpos (verbose, but I don't like primes!).

[Lars]

Thanks for the reply!

I believe the following than works, and should be without Mathlib theorems.

I can put it in lean4/src/Init/Data/Int/DivModLemmas.lean right? If you think this is all good, I'll make a PR.

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

[Kim Morrison]

Thanks!

[Lars]

I've added a PR here: https://github.com/leanprover/lean4/pull/5320

[Kim Morrison]

'd