Theorem: verus_lemma_mod_range (VerusLeanStd/ModInternalsNonlinear.lean)

State before:
x m : ℤ
h : m > 0
⊢ 0 ≤ x % m ∧ x % m < m
Tactic:
have h' : m ≠ 0 := Int.ne_of_gt h
State after:
x m : ℤ
h : m > 0
h' : m ≠ 0
⊢ 0 ≤ x % m ∧ x % m < m

State before:
x m : ℤ
h : m > 0
h' : m ≠ 0
⊢ 0 ≤ x % m ∧ x % m < m
Tactic:
exact ⟨Int.emod_nonneg x h', Int.emod_lt_of_pos x h⟩
State after:
no goals