Theorem: HTPI.mod_nonneg (HTPILib/Chap7.lean)

State before:
m : ℕ
inst✝ : NeZero m
a : ℤ
⊢ 0 ≤ a % ↑m
Tactic:
have h1 : (↑m : Int) ≠ 0 := (Nat.cast_ne_zero).rtl (NeZero.ne m)
State after:
m : ℕ
inst✝ : NeZero m
a : ℤ
h1 : ↑m ≠ 0
⊢ 0 ≤ a % ↑m

State before:
m : ℕ
inst✝ : NeZero m
a : ℤ
h1 : ↑m ≠ 0
⊢ 0 ≤ a % ↑m
Tactic:
show 0 ≤ a % m from Int.emod_nonneg a h1
State after:
no goals