induction xs with
| nil =>
  intro rs
  simp only [filter, filterTR.loop]
  rw [List.length_reverse]
  simp only [length, Nat.zero_add]
  apply Nat.le.refl
| cons x xs ih =>
  intro rs
  simp only [filter, filterTR.loop]
  cases (g x) with
  | true => simp only
            apply Nat.le_trans (ih (x::rs))
            simp only [length]
            rw [Nat.add_comm (length rs), Nat.add_assoc]
            apply Nat.le.refl
  | false => simp only [length]
             apply Nat.le_trans (ih rs)
             rw [Nat.add_comm (length xs) 1,
                 Nat.add_assoc 1,
                 Nat.add_comm 1,
                 Nat.add_one]
             apply Nat.le.step
             apply Nat.le.refl
α : Type u_1
g : α → Bool
xs : List α
⊢ ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
no goals