Theorem: Packet.sum_lt (days/day13.lean)

State before:
x y : Nat
⊢ x < x + y + 1
Tactic:
rw [Nat.add_assoc]
State after:
x y : Nat
⊢ x < x + (y + 1)

State before:
x y : Nat
⊢ x < x + (y + 1)
Tactic:
apply @Nat.add_lt_add_left 0
State after:
case h
x y : Nat
⊢ 0 < y + 1

State before:
case h
x y : Nat
⊢ 0 < y + 1
Tactic:
apply Nat.zero_lt_succ
State after:
no goals