English
For any boolean b and list l with IsChain (≠) on (b :: l), count(!b) l = count(b) l + length(l) mod 2.
Русский
Для булевой переменной b и списка l с свойством IsChain (≠) над (b :: l) выполняется count(¬b) l = count(b) l + length(l) mod 2.
LaTeX
$$$ \forall {b : Bool} {l : List Bool},\; List.IsChain (fun x y => x \neq y) (b :: l) \rightarrow \text{count}(\neg b) l = \text{count}(b) l + \text{length } l \bmod 2 $$$
Lean4
theorem count_not_cons :
∀ {b : Bool} {l : List Bool}, IsChain (· ≠ ·) (b :: l) → count (!b) l = count b l + length l % 2
| _, [], _h => rfl
| b, x :: l, h => by
obtain rfl : b = !x := Bool.eq_not_iff.2 (rel_of_isChain_cons_cons h)
rw [Bool.not_not, count_cons_self, count_cons_of_ne x.not_ne_self.symm,
IsChain.count_not_cons (isChain_cons_of_isChain_cons_cons h), length, add_assoc, Nat.mod_two_add_succ_mod_two]
