proposition: Lemma sink_downwards_crawl: forall L k, weak_heapOrdered_bounded L (1 + k) (1 + k) -> weak_heapOrdered_bounded (sink (L,1 + k)) k k.
proof: Proof. intros. apply sink_hO_bounded in H. rewrite hObU_whObU_pred in H. apply H. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset