It turns out that the chapter of CPDT on General Recursion addresses just that particular issue:
http://adam.chlipala.net/cpdt/html/GeneralRec.html
Read the section called Well-founded recursion, it implements the merge sort using well-founded recursion to help Coq's termination checker be happy.
There may be other ways to solve that problem using either Function
or Program Fixpoint
, but I think reading about well-founded recursion will not hurt.