proposition: Lemma upd_Znth_update {A} {iA : Inhabitant A}: forall t (L: list A) x, 0 <= t < Zlength L -> upd_Znth t L x = update L (Z.to_nat t) x.
proof: Proof. intros. apply List_ext.list_eq_Znth. { rewrite Zlength_upd_Znth. do 2 rewrite Zlength_correct. rewrite update_length. trivial. } intros. rewrite Zlength_upd_Znth in H0. case (eq_dec i t); intros. subst i. rewrite upd_Znth_same; auto. assert (nth_error (update L (Z.to_nat t) x) (Z.to_nat t) = Some x). { rewrite nth_error_update; auto. rewrite Zlength_correct in H. lia. } rewrite Znth_nth_error in H1. inversion H1. do 2 rewrite H3. trivial. rewrite Zlength_correct. rewrite update_length. rewrite Zlength_correct in H. lia. rewrite Znth_upd_Znth_diff; auto. apply nth_error_Znth; auto. rewrite Zlength_correct. rewrite update_length. rewrite Zlength_correct in H0; lia. rewrite nth_error_update'. trivial. lia. Qed.
imports: RelationClasses VST.floyd.proofauto CertiGraph.lib.List_ext CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.binary_heap_malloc_spec CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel