Theorem: remove_mem_length (PnP2023/Labs/Lab02/SelectionSort.lean)

State before:
a : ℕ
l : List ℕ
hyp : a ∈ l
⊢ List.length (List.remove a l) < List.length l
Tactic:
sorry
State after:
no goals