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

State before:
a b x : ℕ
⊢ x ^ (a + b) - x ^ a ≤ (x + 0) ^ (a + b) - (x + 0) ^ a
Tactic:
simp
State after:
no goals