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

State before:
z : ℕ → ℤ
h : StrictMono z
h0 : 0 < z 0
N : ℕ
⊢ N = greatestDPos h ↔ ↑N * z N < (range (N + 1)).sum z ∧ (range (N + 1)).sum z ≤ ↑N * z (N + 1)
Tactic:
rw [eq_greatestDPos_iff h h0, d_succ]
State after:
z : ℕ → ℤ
h : StrictMono z
h0 : 0 < z 0
N : ℕ
⊢ 0 < d z N ∧ (range (N + 1)).sum z - ↑N * z (N + 1) ≤ 0 ↔
    ↑N * z N < (range (N + 1)).sum z ∧ (range (N + 1)).sum z ≤ ↑N * z (N + 1)

State before:
z : ℕ → ℤ
h : StrictMono z
h0 : 0 < z 0
N : ℕ
⊢ 0 < d z N ∧ (range (N + 1)).sum z - ↑N * z (N + 1) ≤ 0 ↔
    ↑N * z N < (range (N + 1)).sum z ∧ (range (N + 1)).sum z ≤ ↑N * z (N + 1)
Tactic:
exact and_congr sub_pos sub_nonpos
State after:
no goals