proposition: Lemma hObU_whObU_pred: forall L k, heapOrdered_bounded L (1 + k) <-> weak_heapOrdered_bounded L k k.
proof: Proof. split; intros. * split; intros. apply H. lia. auto. repeat intro. assert (k > root_idx) by (unfold root_idx in *; lia). generalize (parent_dec k H5). lia. * repeat intro. destruct H. apply H; auto; lia. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset