proposition: Lemma split_permutation: forall l, Permutation ((fst(split l))++snd(split l)) l.
proof: Proof. Proof with auto. intro l; functional induction (split l). - simpl; auto. - simpl; auto. - simpl; constructor ... transitivity ((b::l2)++l1); [apply Permutation_app_comm|]. + simpl; constructor ... transitivity (l1++l2); [apply Permutation_app_comm|]. now rewrite e0 in IHp; simpl in IHp. Qed.
imports: Coq(List Wf_nat Recdef Compare_dec Arith Peano_dec Lia RelationClasses Sorting.Sorted Sorting.Permutation) hydras(DecPreOrder DecPreOrder_Instances Sort_spec)