proposition: Lemma heapOrdered_raise_priority_weak_heapOrdered: forall H, heapOrdered H -> forall t old, nth_error H t = Some old -> forall new, old <<= new -> weak_heapOrdered (update H t new) t.
proof: Proof. split; intros. rewrite nth_error_update' in H4; auto. specialize (H0 _ _ H4). destruct H0. case (eq_nat_dec t (left_child i)); intro. subst t. rewrite nth_error_update. 2: apply nth_error_Some; intro Hx; rewrite Hx in H1; discriminate. rewrite nth_error_update'. 2: apply left_child_neq_right_child. split; intros; auto. inversion H6. subst b. transitivity old; auto. case (eq_nat_dec t (right_child i)); intro. subst t. rewrite nth_error_update. 2: apply nth_error_Some; intro Hx; rewrite Hx in H1; discriminate. rewrite nth_error_update'. 2: { intro. symmetry in H6. apply left_child_neq_right_child in H6; trivial. } split; intros; auto. inversion H6. subst c. transitivity old; auto. rewrite nth_error_update'; auto. rewrite nth_error_update'; auto. repeat intro. rewrite nth_error_update' in H7. 2: generalize (parent_dec t); lia. rewrite nth_error_update' in H6. 2: intro; subst gs; generalize (parent_dec t); lia. apply hOhO2 in H0. transitivity old; eapply H0; eauto. rewrite H5; trivial. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset