proposition: Lemma Znth_Zexchange'' : forall {A} `{Ia : Inhabitant A} (L : list A) k i j, 0 <= i < Zlength L -> 0 <= j < Zlength L -> k <> i -> k <> j -> Znth k (Zexchange L i j) = Znth k L.
proof: Proof. intros. assert (k < 0 \/ 0 <= k < Zlength L \/ Zlength L <= k) by lia. destruct H3 as [? | [? | ?]]. repeat rewrite Znth_underflow; trivial. 2: repeat rewrite Znth_overflow; try rewrite Zlength_Zexchange; trivial; lia. apply nth_error_Znth; auto. rewrite Zlength_Zexchange. trivial. apply nth_error_exchange''. intro. apply H1. apply Z2Nat.inj; lia. intro. apply H2. apply Z2Nat.inj; lia. Qed.
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap_model