proposition: Theorem stable_mergesort_OK : sort_spec stable_merge_sort.
proof: Proof. red; intros. now destruct (merge_sort_correct A le P _ (split' _) (split'_decr _) (split'_permutation _) l). Qed.
imports: Coq(List Wf_nat Recdef Compare_dec Arith Peano_dec Lia RelationClasses Sorting.Sorted Sorting.Permutation) hydras(DecPreOrder DecPreOrder_Instances Sort_spec)