proposition: Lemma heapOrdered_lower_priority_weak_heapOrdered2: forall H, heapOrdered H -> forall t old, nth_error H t = Some old -> forall new, new <<= old -> weak_heapOrdered2 (update H t new) t.
proof: Proof. intros. apply hOhO2 in H0. split. intros. rewrite nth_error_update' in H4; auto. case (dec_eq_nat t (parent i)); intro. subst t. rewrite nth_error_update in H5. inversion H5. subst a. clear H5. transitivity old; auto. eapply H0; eauto. eapply nth_error_Some. intro. rewrite H6 in H1. discriminate. rewrite nth_error_update' in H5; auto. eapply H0; eauto. repeat intro. assert (t > root_idx) by (unfold root_idx in *; lia). generalize (parent_dec _ H8); intro. rewrite nth_error_update' in H7. 2: lia. rewrite nth_error_update' in H6. transitivity old; eapply H0; eauto. rewrite H5; trivial. intro. subst gs. lia. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset