proposition: Lemma partition_list_permut1 : forall e l, let (l1,l2) := partition e l in permut (l1 ++ l2) l.
proof: Proof. intros e l; functional induction (partition e l) as [|H1 e' l' H2 IH l1 l2 rec_res e'_lt_e|H1 e' l' H2 IH l1 l2 rec_res H3]. auto. simpl app; rewrite rec_res in IH; rewrite IH; auto. simpl app; rewrite rec_res in IH; apply permut_sym; rewrite <- permut_cons_inside; auto. reflexivity. Qed.
imports: Coq(Relations Setoid List Multiset Arith Recdef Morphisms) CoLoR(more_list list_permut ordered_set)