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

State before:
a b : ℕ
h : b ≠ 0
⊢ a % b < b
Tactic:
have h1 : b > 0 := Nat.pos_of_ne_zero h
State after:
a b : ℕ
h : b ≠ 0
h1 : b > 0
⊢ a % b < b

State before:
a b : ℕ
h : b ≠ 0
h1 : b > 0
⊢ a % b < b
Tactic:
show a % b < b from Nat.mod_lt a h1
State after:
no goals