sort a formally verified mergesort implementation in Coq compatibility written and tested with Coq 8.8.0