proposition: Lemma insert_permutation: forall L x, Permutation (x :: L) (insert L x).
proof: Proof. intros. unfold insert. transitivity (L ++ (x :: nil)). change (x :: L) with ((x :: nil) ++ L). apply Permutation_app_comm. apply swim_permutation. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset