count_not_le_count_add_one — Mathlib

English

For hl a chain (Ne) on l, for any boolean b, count(!b) l ≤ count(b) l + 1.

Русский

Для hl — цепочки (Ne) на l, для любого b: count(!b) l ≤ count(b) l + 1.

LaTeX

$$$ \forall {l : List Bool},\; hl : List.IsChain (fun x y => x \neq y) l \rightarrow \forall (b : Bool),\; count(¬ b) l \le count(b) l + 1 $$$

Lean4

theorem count_not_le_count_add_one (hl : IsChain (· ≠ ·) l) (b : Bool) : count (!b) l ≤ count b l + 1 :=
  by
  rcases l with - | ⟨x, l⟩
  · exact zero_le _
  obtain rfl | rfl : b = x ∨ b = !x := by simp only [Bool.eq_not_iff, em]
  · rw [count_cons_of_ne b.not_ne_self.symm, count_cons_self, hl.count_not_cons, add_assoc]
    cutsat
  · rw [Bool.not_not, count_cons_self, count_cons_of_ne x.not_ne_self.symm, hl.count_not_cons]
    cutsat

Похожие утверждения