apply Nat.le.step
case cons.false
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length (filter g xs) ≤ length (x :: xs)
case cons.false.a
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ Nat.le (length (filter g xs)) (length xs)