Theorem: verus_lemma_small_div (VerusLeanStd/DivInternalsNonlinear.lean)

State before:
⊢ ∀ (x d : ℤ), 0 ≤ x ∧ x < d ∧ d > 0 → x / d = 0
Tactic:
intro x d h
State after:
x d : ℤ
h : 0 ≤ x ∧ x < d ∧ d > 0
⊢ x / d = 0

State before:
x d : ℤ
h : 0 ≤ x ∧ x < d ∧ d > 0
⊢ x / d = 0
Tactic:
exact Int.ediv_eq_zero_of_lt h.1 h.2.1
State after:
no goals