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