Kata

Last time we proved a random fact about filtering. Here's another one: given two predicates f, g, the number of elements satisfying both cannot exceed that satisfying either.

forall (X : Type) (l : list X) (f g : X -> bool),
  length (filter (fun x => f x && g x) l) <= length (filter f l) /\
  length (filter (fun x => f x && g x) l) <= length (filter g l)

universe u

∀ {α : Type u} {p q : α → Prop} [decidable_pred p]
  [decidable_pred q] {L: list α}, 
  (L.filter $ λ x, p x ∧ q x).length ≤ (L.filter p).length ∧
    (L.filter $ λ x, p x ∧ q x).length ≤ (L.filter q).length

Prove it.