l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ length l - (2 - 1) ≤ 2 * count b l
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ length l / 2 ≤ count b l
rw [Nat.div_le_iff_le_mul_add_pred two_pos, ← tsub_le_iff_right]
no goals
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ length l - (2 - 1) ≤ 2 * count b l
exact length_sub_one_le_two_mul_count_bool hl b