proposition: Lemma split'_aux_length_fst: forall l l', length(fst(split'_aux l l')) = min (Nat.div2(length l')) (length l).
proof: Proof. intros; functional induction (split'_aux l l'); simpl. + rewrite e1 in IHp; simpl in IHp. abstract lia. + destruct l; destruct l'; simpl; auto. now rewrite Nat.min_0_r. destruct l'; simpl; auto. contradiction. Qed.
imports: Coq(List Wf_nat Recdef Compare_dec Arith Peano_dec Lia RelationClasses Sorting.Sorted Sorting.Permutation) hydras(DecPreOrder DecPreOrder_Instances Sort_spec)