Theorem: IMOSL.IMO2017A4.good2_bdd_below (IMOSLLean4/IMO2017/A4/A4.lean)

State before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D n : ℕ
a : ℕ → G
h : good2 D a
h0 : D ≤ n
⊢ -a (n + 1) ≤ 2 • Extra.seqMax a n
Tactic:
rcases h n h0 with ⟨i, j, rfl, h0⟩
State after:
case intro.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D : ℕ
a : ℕ → G
h : good2 D a
i j : ℕ
h0✝ : D ≤ i + j
h0 : a (i + j + 1) = -(a i + a j)
⊢ -a (i + j + 1) ≤ 2 • Extra.seqMax a (i + j)

State before:
case intro.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D : ℕ
a : ℕ → G
h : good2 D a
i j : ℕ
h0✝ : D ≤ i + j
h0 : a (i + j + 1) = -(a i + a j)
⊢ -a (i + j + 1) ≤ 2 • Extra.seqMax a (i + j)
Tactic:
rw [h0, neg_neg, two_nsmul]
State after:
case intro.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D : ℕ
a : ℕ → G
h : good2 D a
i j : ℕ
h0✝ : D ≤ i + j
h0 : a (i + j + 1) = -(a i + a j)
⊢ a i + a j ≤ Extra.seqMax a (i + j) + Extra.seqMax a (i + j)

State before:
case intro.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D : ℕ
a : ℕ → G
h : good2 D a
i j : ℕ
h0✝ : D ≤ i + j
h0 : a (i + j + 1) = -(a i + a j)
⊢ a i + a j ≤ Extra.seqMax a (i + j) + Extra.seqMax a (i + j)
Tactic:
exact add_le_add (Extra.le_seqMax_of_le a (i.le_add_right j))
  (Extra.le_seqMax_of_le a (j.le_add_left i))
State after:
no goals