n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
⊢ ∃ i, j < sizeUpTo c (Nat.succ i) ∧ i < length c
n : ℕ
c : Composition n
j : ℕ
h : j < n
⊢ ∃ i, j < sizeUpTo c (Nat.succ i) ∧ i < length c
have n_pos : 0 < n := lt_of_le_of_lt (zero_le j) h
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
this : 0 < sum c.blocks
⊢ ∃ i, j < sizeUpTo c (Nat.succ i) ∧ i < length c
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
⊢ ∃ i, j < sizeUpTo c (Nat.succ i) ∧ i < length c
have : 0 < c.blocks.sum := by rwa [← c.blocks_sum] at n_pos
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
this : 0 < sum c.blocks
length_pos : 0 < List.length c.blocks
⊢ ∃ i, j < sizeUpTo c (Nat.succ i) ∧ i < length c
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
this : 0 < sum c.blocks
⊢ ∃ i, j < sizeUpTo c (Nat.succ i) ∧ i < length c
have length_pos : 0 < c.blocks.length := length_pos_of_sum_pos (blocks c) this
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
this : 0 < sum c.blocks
length_pos : 0 < List.length c.blocks
⊢ j < sizeUpTo c (Nat.succ (Nat.pred (length c)))
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
this : 0 < sum c.blocks
length_pos : 0 < List.length c.blocks
⊢ ∃ i, j < sizeUpTo c (Nat.succ i) ∧ i < length c
refine' ⟨c.length.pred, _, Nat.pred_lt (ne_of_gt length_pos)⟩
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
this✝ : 0 < sum c.blocks
length_pos : 0 < List.length c.blocks
this : Nat.succ (Nat.pred (length c)) = length c
⊢ j < sizeUpTo c (Nat.succ (Nat.pred (length c)))
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
this : 0 < sum c.blocks
length_pos : 0 < List.length c.blocks
⊢ j < sizeUpTo c (Nat.succ (Nat.pred (length c)))
have : c.length.pred.succ = c.length := Nat.succ_pred_eq_of_pos length_pos
no goals
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
this✝ : 0 < sum c.blocks
length_pos : 0 < List.length c.blocks
this : Nat.succ (Nat.pred (length c)) = length c
⊢ j < sizeUpTo c (Nat.succ (Nat.pred (length c)))
simp [this, h]
no goals
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
⊢ 0 < sum c.blocks
rwa [← c.blocks_sum] at n_pos