proposition: Lemma hOhO2: forall L, heapOrdered L <-> heapOrdered2 L.
proof: Proof. split; repeat intro. * destruct i. simpl in H1. destruct L. discriminate. inversion H1. simpl in H0. inversion H0. subst. reflexivity. specialize (H _ _ H1). destruct H. destruct (even_or_odd (S i)). apply H2. rewrite right_child_parent_even; auto. unfold root_idx; lia. apply H. rewrite left_child_parent_odd; auto. * split; intros; eapply H; try apply H1. rewrite parent_left_child. trivial. rewrite parent_right_child. trivial. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset