Theorem: IMOSL.IMO2014A1.binom_bound (IMOSLLean4/IMO2014/A1/A1.lean)

State before:
z : ℕ → ℤ
h : StrictMono z
n : ℕ
⊢ d z (n + 1) ≤ z 0 - ↑((n + 1).choose 2)
Tactic:
rw [Nat.choose, Nat.choose_one_right, Nat.cast_add,
  ← sub_sub, sub_right_comm]
State after:
z : ℕ → ℤ
h : StrictMono z
n : ℕ
⊢ d z (n + 1) ≤ z 0 - ↑(n.choose (1 + 1)) - ↑n

State before:
z : ℕ → ℤ
h : StrictMono z
n : ℕ
⊢ d z (n + 1) ≤ z 0 - ↑(n.choose (1 + 1)) - ↑n
Tactic:
exact Int.le_sub_right_of_add_le <|
  (Int.add_le_of_le_sub_right (main_lemma h n)).trans (binom_bound n)
State after:
no goals