proposition: Lemma heapify_permutation: forall L, Permutation L (heapify L).
proof: Proof. intros. apply build_heap_permutation. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset