Theorem: blah2 (HMem/Trace/Master.lean)

State before:
a x : ℕ
⊢ (x + 1) ^ a - x ^ a ≤ (x + 1) ^ (a + 1) - x ^ (a + 1)
Tactic:
apply Nat.sub_le_of_le_add
State after:
case h
a x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + 1) - x ^ (a + 1) + x ^ a

State before:
case h
a x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + 1) - x ^ (a + 1) + x ^ a
Tactic:
rw [← Nat.sub_add_comm]
State after:
case h
a x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + 1) + x ^ a - x ^ (a + 1)

case h
a x : ℕ
⊢ x ^ (a + 1) ≤ (x + 1) ^ (a + 1)

State before:
case h
a x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + 1) + x ^ a - x ^ (a + 1)

case h
a x : ℕ
⊢ x ^ (a + 1) ≤ (x + 1) ^ (a + 1)
Tactic:
apply Nat.le_sub_of_add_le
State after:
case h.h
a x : ℕ
⊢ (x + 1) ^ a + x ^ (a + 1) ≤ (x + 1) ^ (a + 1) + x ^ a

case h
a x : ℕ
⊢ x ^ (a + 1) ≤ (x + 1) ^ (a + 1)

State before:
case h.h
a x : ℕ
⊢ (x + 1) ^ a + x ^ (a + 1) ≤ (x + 1) ^ (a + 1) + x ^ a

case h
a x : ℕ
⊢ x ^ (a + 1) ≤ (x + 1) ^ (a + 1)
Tactic:
apply blah
State after:
case h
a x : ℕ
⊢ x ^ (a + 1) ≤ (x + 1) ^ (a + 1)

State before:
case h
a x : ℕ
⊢ x ^ (a + 1) ≤ (x + 1) ^ (a + 1)
Tactic:
apply Nat.pow_le_pow_left
State after:
case h.h
a x : ℕ
⊢ x ≤ x + 1

State before:
case h.h
a x : ℕ
⊢ x ≤ x + 1
Tactic:
apply Nat.le_add_right
State after:
no goals