proposition: Lemma heapify_builds_heap: forall L, heapOrdered (heapify L).
proof: Proof. unfold heapify. intros. apply build_heap_helper_downwards. apply hObU_whObU_pred, heapOrdered_bounded_half. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset