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