proposition: Lemma upd_Znth_overwrite: forall {A} (l : list A) i a b, 0 <= i < Zlength l -> upd_Znth i (upd_Znth i l a) b = upd_Znth i l b.
proof: Proof. intros. rewrite upd_Znth_unfold by now rewrite upd_Znth_Zlength. rewrite upd_Znth_Zlength; trivial. repeat rewrite upd_Znth_unfold by trivial. rewrite sublist0_app1. 2: rewrite Zlength_sublist; lia. rewrite sublist_sublist00 by lia. f_equal. f_equal. rewrite app_assoc. rewrite sublist_app2. 2: { rewrite Zlength_app, Zlength_sublist by lia. unfold Zlength. simpl. lia. } rewrite Zlength_app, Zlength_sublist by lia. unfold Zlength at 1; simpl. rewrite sublist_same; trivial. - lia. - unfold Zlength at 2; simpl. rewrite Zlength_sublist by lia. lia. Qed.
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap_model