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