. rewrite [Nat.succ_add]; exact Nat.succ_le_succ <| .step IH
case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + (countP q l + 1)
no goals