Theorem: verus_lemma_mod_of_zero_is_zero (VerusLeanStd/ModInternalsNonlinear.lean)

State before:
m : ℤ
h : 0 < m
⊢ 0 % m = 0
Tactic:
rfl
State after:
no goals