cases Nat.eq_or_lt_of_le (IH hl.tail) with
| inl hone =>
  have ⟨b,hb⟩:= (countP_pos p).mp (trans Nat.zero_lt_one hone.symm)
  rewrite [hone, Nat.add_comm]
  apply Nat.succ_le_succ
  if hpa : p a = true then
    have : a = b := hp _ _ hpa hb.2
    cases this
    exact absurd hb.1 hl.head
  else
    rewrite [if_neg hpa]; exact .refl
| inr hlt =>
  have := Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ hlt)
  rewrite [this, Nat.zero_add]
  cases p a <;> decide
case cons
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
⊢ (countP p l + if p a = true then 1 else 0) ≤ 1
no goals