proposition: Lemma swim_permutation: forall L j, Permutation L (swim L j).
proof: Proof. intros. apply swim_ind; clear; intros. generalize (swim1_permutation L j); intro. rewrite e in H. trivial. generalize (swim1_permutation L j); intro. rewrite e in H0. transitivity L'; trivial. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset