Coq-style implementation of Insertion sort

2 Likes