proposition: Lemma build_heap_permutation: forall L n, Permutation L (build_heap_helper L n).
proof: Proof. intros L n. revert L. induction n; intros. simpl. apply sink_permutation. simpl. eapply Permutation_trans. 2: apply IHn. apply sink_permutation. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset