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

State before:
m : ℕ
inst✝ : NeZero m
a : ℤ
⊢ a % ↑m < ↑m
Tactic:
have h1 : m > 0 := Nat.pos_of_ne_zero (NeZero.ne m)
State after:
m : ℕ
inst✝ : NeZero m
a : ℤ
h1 : m > 0
⊢ a % ↑m < ↑m

State before:
m : ℕ
inst✝ : NeZero m
a : ℤ
h1 : m > 0
⊢ a % ↑m < ↑m
Tactic:
have h2 : (↑m : Int) > 0 := (Nat.cast_pos).rtl h1
State after:
m : ℕ
inst✝ : NeZero m
a : ℤ
h1 : m > 0
h2 : ↑m > 0
⊢ a % ↑m < ↑m

State before:
m : ℕ
inst✝ : NeZero m
a : ℤ
h1 : m > 0
h2 : ↑m > 0
⊢ a % ↑m < ↑m
Tactic:
show a % m < m from Int.emod_lt_of_pos a h2
State after:
no goals