Draft: small proofs to pick up the ropes
This is my first attempt, not sure it should be merged. It includes the following:
- definitions for last and last_opt in
Environments/List.v
- a new file
Proofs/List.v
with 3 lemmas.
Edited by Guillaume Claret