α : Type u_1
l : List α
inst✝ : DecidableEq α
head : α
tail : List α
a : α
h : 0 < length (head :: tail)
⊢ count a (List.tail (head :: tail)) =
    (count a tail + if a = head then 1 else 0) - if a = get (head :: tail) { val := 0, isLt := h } then 1 else 0
α : Type u_1
l : List α
inst✝ : DecidableEq α
head : α
tail : List α
a : α
h : 0 < length (head :: tail)
⊢ count a (List.tail (head :: tail)) =
    count a (head :: tail) - if a = get (head :: tail) { val := 0, isLt := h } then 1 else 0
rw [count_cons']
no goals
α : Type u_1
l : List α
inst✝ : DecidableEq α
head : α
tail : List α
a : α
h : 0 < length (head :: tail)
⊢ count a (List.tail (head :: tail)) =
    (count a tail + if a = head then 1 else 0) - if a = get (head :: tail) { val := 0, isLt := h } then 1 else 0
split_ifs <;> simp at * <;> contradiction