simp only [length]
case cons.true
α : 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 (x :: rs) ≤ length (x :: xs) + length rs
case cons.true
α : 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 + 1) ≤ length xs + 1 + length rs