α : Type u_1
l₁ l₂ : List α
n : Nat
h₁ : length l₁ ≤ n
h₂ : n < length l₁ + length l₂
⊢ n - length l₁ < length l₂
α : Type u_1
l₁ l₂ : List α
n : Nat
h₁ : length l₁ ≤ n
h₂ : n < length (l₁ ++ l₂)
⊢ n - length l₁ < length l₂
rw [length_append] at h₂
no goals
α : Type u_1
l₁ l₂ : List α
n : Nat
h₁ : length l₁ ≤ n
h₂ : n < length l₁ + length l₂
⊢ n - length l₁ < length l₂
exact Nat.sub_lt_left_of_lt_add h₁ h₂