proposition: Lemma weak_heapOrdered2_oob: forall i L, i >= length L -> weak_heapOrdered2 L i -> heapOrdered L.
proof: Proof. intros. apply hOhO2. repeat intro. destruct H0. eapply H0. 2: apply H1. 2: apply H2. 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