Lab02: Selection Sort (part 1) and `≤` on `Answer`
due by Monday, Feb 6, 2023
Before doing this assignment you will need to pull from the upstream repository, i.e., the course repository. Please complete the definitions/proofs in the files PnP2023/Labs/Lab02/SelectionSort.lean
and PnP2023/Labs/Lab02/AnswerLE.lean
. When you are done please commit and push your changes to your forked private repository and alert me on Zulip.

Complete the proof of
remove_length_le
inPnP2023/Labs/Lab02/SelectionSort.lean
. 
Complete the proof of
remove_mem_length
inPnP2023/Labs/Lab02/SelectionSort.lean
. 
Complete the definition of
selectionSort
inPnP2023/Labs/Lab02/SelectionSort.lean
, including proof by termination. Do not make this apartial def
. Also ensure that there is no error saying that you failed to prove termination. 
Complete the proof of
Answer.eq_of_le_le
inPnP2023/Labs/Lab02/AnswerLE.lean
.