proposition: Lemma heapOrdered_bounded_root_heapOrdered: forall L, heapOrdered_bounded L root_idx <-> heapOrdered L.
proof: Proof. split. split; intros; assert (i >= root_idx) by (unfold root_idx; lia); destruct (H i a H2 H0); auto. repeat intro. apply H. trivial. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset