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

State before:
z : ℕ → ℤ
h : StrictMono z
n : ℕ
⊢ d z (n + 1) ≤ d z n - ↑n
Tactic:
rw [d_succ, d, sub_sub, ← mul_add_one (α := ℤ)]
State after:
z : ℕ → ℤ
h : StrictMono z
n : ℕ
⊢ (range (n + 1)).sum z - ↑n * z (n + 1) ≤ (range (n + 1)).sum z - ↑n * (z n + 1)

State before:
z : ℕ → ℤ
h : StrictMono z
n : ℕ
⊢ (range (n + 1)).sum z - ↑n * z (n + 1) ≤ (range (n + 1)).sum z - ↑n * (z n + 1)
Tactic:
exact Int.sub_le_sub_left
  (Int.mul_le_mul_of_nonneg_left (h n.lt_succ_self) (Int.ofNat_zero_le n)) _
State after:
no goals