Theorem: verus_lemma_0_mod_any (VerusLeanStd/ModInternalsNonlinear.lean)

State before:
⊢ ∀ m > 0, 0 % m = 0
Tactic:
intros
State after:
m✝ : ℤ
a✝ : m✝ > 0
⊢ 0 % m✝ = 0

State before:
m✝ : ℤ
a✝ : m✝ > 0
⊢ 0 % m✝ = 0
Tactic:
rfl
State after:
no goals