proposition: Lemma weak_heapOrdered_bounded_half: forall L, weak_heapOrdered_bounded L (parent (length L)) (parent (length L)).
proof: Proof. intros. rewrite <- hObU_whObU_pred. apply heapOrdered_bounded_half. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset