proposition: Lemma heapOrdered_bounded_half: forall L, heapOrdered_bounded L (1 + parent (length L)).
proof: Proof. intro. assert (length L = 0 \/ length L > 0) by lia. destruct H. destruct L. repeat intro. destruct i; inversion H1. inversion H. rename H into Hx. split; repeat intro. * assert (left_child i < length L) by (apply nth_error_Some; congruence). destruct (even_or_odd (length L)). + apply right_child_monotone in H. rewrite right_child_parent_even in H; auto. clear -H H2. generalize (left_child_S_right_child i); intro. lia. + apply left_child_monotone in H. rewrite left_child_parent_odd in H; auto. lia. * assert (right_child i < length L) by (apply nth_error_Some; congruence). destruct (even_or_odd (length L)). + apply right_child_monotone in H. rewrite right_child_parent_even in H; auto. lia. + apply left_child_monotone in H. rewrite left_child_parent_odd in H; auto. assert (Hw : left_child i < right_child i) by apply left_child_lt_right_child. lia. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset