l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ length l - 1 ≤ if Even (length l) then length l else if (some b == head? l) = true then length l + 1 else length l - 1
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ length l - 1 ≤ 2 * count b l
rw [hl.two_mul_count_bool_eq_ite]
no goals
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ length l - 1 ≤ if Even (length l) then length l else if (some b == head? l) = true then length l + 1 else length l - 1
split_ifs <;> simp [le_tsub_add, Nat.le_succ_of_le]