proposition: Lemma sink_hO_bounded: forall L k j, weak_heapOrdered_bounded L k j -> heapOrdered_bounded (sink (L, j)) k.
proof: Proof. intros L k j whO. remember (L, j) as Lj. assert (match Lj with (L, j) => weak_heapOrdered_bounded L k j end). rewrite HeqLj. trivial. revert H. clear -Apo Aleq_linear. apply sink_ind; intros. generalize (sink1_hObU L k j H). rewrite e0. trivial. generalize (sink1_hObU L k j H0). rewrite e0. apply H. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset