List.count_not_add_count
theorem List.count_not_add_count : ∀ (l : List Bool) (b : Bool), List.count (!b) l + List.count b l = l.length := by
sorry
This theorem states that for any list of Boolean values, the total count of occurrences of a Boolean value and its negation in the list equals the length of the list. In other words, if you sum the number of times a particular boolean (either `true` or `false`) and its opposite appear in a list, you will always get the total number of elements in the list.
More concisely: For any list of Boolean values, the sum of the count of each Boolean value and its negation is equal to the length of the list.
|