Theorem: List.drop_isInfix_drop (One.lean)

State before:
n m : ℕ
α✝ : Type u_1
l : List α✝
h : n ≥ m
⊢ drop n l <:+: drop m l
Tactic:
rw [← Nat.add_sub_of_le h, add_comm, List.drop_add]
State after:
n m : ℕ
α✝ : Type u_1
l : List α✝
h : n ≥ m
⊢ drop (n - m) (drop m l) <:+: drop m l

State before:
n m : ℕ
α✝ : Type u_1
l : List α✝
h : n ≥ m
⊢ drop (n - m) (drop m l) <:+: drop m l
Tactic:
apply List.drop_isInfix
State after:
no goals