proposition: Lemma sink_permutation: forall L j, Permutation L (sink (L,j)).
proof: Proof. intros. remember (L, j) as Lj. replace L with (match Lj with (L, _) => L end) by (subst; trivial). clear. apply sink_ind; intros. generalize (sink1_permutation L j); intro. rewrite e0 in H. trivial. generalize (sink1_permutation L j); intro. rewrite e0 in H0. transitivity L'; trivial. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset