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

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

State before:
x y : Nat
⊢ x < x + y + 1
Tactic:
apply sum_lt
State after:
no goals