Theorem: Algdata.BinaryHeap.lt_child_left (Algdata/Data/BinaryHeap/Index.lean)

State before:
i : Nat
⊢ i < 2 * i + 1
Tactic:
rewrite [Nat.two_mul]
State after:
i : Nat
⊢ i < i + i + 1

State before:
i : Nat
⊢ i < i + i + 1
Tactic:
exact Nat.succ_le_succ (i.le_add_left i)
State after:
no goals