Added reference to journal article.
[2018-09-17] Added theory Efficient_Mergesort that works exclusively with the mutual induction schemas generated by the function package.
[2018-09-19] Added theory Mergesort_Complexity that proves an upper bound on the number of comparisons that are required by mergesort.
[2018-09-19] Theory Efficient_Mergesort replaces theory Efficient_Sort but keeping the old name Efficient_Sort. [2020-11-20] Additional theory Natural_Mergesort that developes an efficient mergesort algorithm without key-functions for educational purposes.