a/b=0 in integers

Stream: Is there code for X?

[Kevin Buzzard]

Is this true, and do we have it if so?

import Mathlib.Tactic

example (a b : ℤ) : a / b = 0 ↔ b = 0 ∨ (0 ≤ a ∧ a < |b|) := by
  sorry

A student just needed the direction I couldn't find. In fact I couldn't even find this:

example (a b : ℤ) (h1 : 0 < b) (h2 : b ≤ a) : 1 ≤ a / b := by sorry

Reminder: lemmas about integer division have ediv not div in the name.

[Alex J. Best]

I would hope slim check would find a counterexample if its not true?

[Damiano Testa]

It seems to be true for a, b in [-1000,1000]:

#eval
  Id.run do
  let mut cond := true
  for sa in [0:1] do
    for sb in [0:1] do
      for a' in [0:1000] do
        for b' in [0:1000] do
        let a : ℤ := (2 * sa - 1) / 2 * a'
        let b : ℤ := (2 * sb - 1) / 2 * b'
        cond := cond && decide (a / b = 0 ↔ b = 0 ∨ (0 ≤ a ∧ a < |(b : ℤ)|))
  return cond

[Alex J. Best]

And the direction you asked about follows from docs#Int.le_ediv_of_mul_le

[Eric Wieser]

@Damiano Testa, here's another way to check it (but sadly with much smaller bounds):

example :
  ∀ a ∈ Finset.Icc (-10) 10, ∀ b ∈ Finset.Icc (-10) 10,
    a / b = 0 ↔ b = 0 ∨ (0 ≤ a ∧ a < |(b : ℤ)|) := by decide