proposition: Lemma swim1_permutation: forall L j, match swim1 L j with | (L', _) => Permutation L L' end.
proof: Proof. unfold swim1. intros. case (j <=? root_idx); auto. case (nth_error L j); auto. case (nth_error L (parent j)); auto. intros. case (a0 <<=? a); auto. intro. symmetry. apply exchange_Permutation. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset