proposition: Lemma weak_heapOrdered2_root: forall (L : list A), weak_heapOrdered2 L root_idx -> heapOrdered L.
proof: Proof. intros. rewrite hOhO2. repeat intro. destruct H. case (eq_nat_dec i root_idx); intro. subst i. rewrite parent_root in H1. rewrite H0 in H1. inversion H1. reflexivity. eapply H; eauto. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset