proposition: Lemma split'_permutation: forall l, Permutation ((fst(split' l))++snd(split' l)) l.
proof: Proof. intro; unfold split'; rewrite split'_aux_eq; trivial. Qed.
imports: Coq(List Wf_nat Recdef Compare_dec Arith Peano_dec Lia RelationClasses Sorting.Sorted Sorting.Permutation) hydras(DecPreOrder DecPreOrder_Instances Sort_spec)