proposition: Lemma sink_hO: forall L j, weak_heapOrdered L j -> heapOrdered (sink (L, j)).
proof: Proof. intros. rewrite <- heapOrdered_bounded_root_heapOrdered. apply sink_hO_bounded. rewrite weak_heapOrdered_bounded_root_weak_heapOrdered. trivial. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset