induction l with
| nil => exact .refl
| cons a l IH =>
  simp only [countP_cons]
  cases p a <;> cases q a <;> simp only [ite_true, ite_false, Nat.add_zero]
  . exact IH
  . exact Nat.succ_le_succ IH
  . rewrite [Nat.succ_add]; exact Nat.succ_le_succ IH
  . rewrite [Nat.succ_add]; exact Nat.succ_le_succ <| .step IH
α : Type u
β : Type v
p q : α → Bool
l : List α
⊢ countP (fun a => p a || q a) l ≤ countP p l + countP q l
no goals