proposition: Lemma split'_aux_length_preserve: forall l l', length(fst(split'_aux l l')) + length(snd (split'_aux l l')) = length l.
proof: Proof. intros; functional induction (split'_aux l l'); simpl. + rewrite e1 in IHp; simpl in IHp. now rewrite IHp. + 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)