rewrite [Nat.succ_add]
case cons.true.false
α : 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
case cons.true.false
α : 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 ≤ Nat.succ (countP p l + countP q l)