proposition: Lemma upd_Znth_Zexchange {A} {iA : Inhabitant A}: forall k j (L : list A), 0 <= k < Zlength L -> 0 <= j < Zlength L -> upd_Znth k (upd_Znth j L (Znth k L)) (Znth j L) = Zexchange L j k.
proof: Proof. intros. apply list_eq_Znth; do 2 rewrite Zlength_upd_Znth. rewrite Zlength_Zexchange; trivial. intros. case (Z.eq_dec i k); intro. * subst k. rewrite Znth_Zexchange'; auto. rewrite upd_Znth_same; auto. rewrite Zlength_upd_Znth; auto. * rewrite upd_Znth_diff; auto. 2,3: rewrite Zlength_upd_Znth; auto. case (Z.eq_dec i j); intro. + subst j. rewrite upd_Znth_same; auto. rewrite Znth_Zexchange; auto. + rewrite upd_Znth_diff; auto. rewrite Znth_Zexchange''; auto. 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