Stuff for data.nat.choose.basic

theorem Nat.choose_add_le_pow_left (s t : ℕ) : (s + t).choose s ≤ (t + 1) ^ s

theorem Nat.choose_le_pow_left (s t : ℕ) : s.choose t ≤ (s + 1 - t) ^ t