apply Nat.le.refl
case cons.false.a
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ Nat.le (length xs + length rs) (length xs + length rs)
no goals