Theorem: verus_lemma_div_basics (VerusLeanStd/DivInternals.lean)

State before:
n : ℤ
h : n > 0
⊢ n / n = 1 ∧
    (-(-n / n) == 1) = true ∧
      (∀ (x : ℤ), 0 ≤ x ∧ x < n ↔ x / n = 0) ∧ (∀ (x : ℤ), (x + n) / n = x / n + 1) ∧ ∀ (x : ℤ), (x - n) / n = x / n - 1
Tactic:
sorry
State after:
no goals