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

State before:
a n : ℕ
⊢ a % (n + 1) < n + 1
Tactic:
have h : n + 1 > 0 := Nat.succ_pos n
State after:
a n : ℕ
h : n + 1 > 0
⊢ a % (n + 1) < n + 1

State before:
a n : ℕ
h : n + 1 > 0
⊢ a % (n + 1) < n + 1
Tactic:
show a % (n + 1) < n + 1 from Nat.mod_lt a h
State after:
no goals