proposition: Lemma weak_heapOrdered_bounded_oob: forall i L b, i >= length L -> weak_heapOrdered_bounded L b i -> heapOrdered_bounded L b.
proof: Proof. repeat intro. destruct H0. apply H0; auto. intro. subst i0. assert (i < length L) by (apply nth_error_Some; congruence). lia. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset