English
If hl is a chain (Ne) and length l is Even, then for any b, count(!b) l = count(b) l.
Русский
Если hl образует цепочку по неравенству и длина l четна, то для любого b справедливо count(!b) l = count(b) l.
LaTeX
$$$ \forall {l : List Bool},\; hl : List.IsChain (fun x y => x \neq y) l \rightarrow Even (length l) \rightarrow \forall (b : Bool),\; count(\neg b) l = count(b) l $$$
Lean4
theorem count_not_eq_count (hl : IsChain (· ≠ ·) l) (h2 : Even (length l)) (b : Bool) : count (!b) l = count b l :=
by
rcases l with - | ⟨x, l⟩
· rfl
rw [length_cons, Nat.even_add_one, Nat.not_even_iff] at h2
suffices count (!x) (x :: l) = count x (x :: l) by grind
rw [count_cons_of_ne x.not_ne_self.symm, hl.count_not_cons, h2, count_cons_self]
