proposition: Lemma weak_heapOrdered_oob: forall i L, i >= length L -> weak_heapOrdered L i -> heapOrdered L.
proof: Proof. intros. apply weak_heapOrdered_bounded_root_weak_heapOrdered in H0. apply heapOrdered_bounded_root_heapOrdered. apply weak_heapOrdered_bounded_oob in H0; auto. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset