proposition: Lemma Znth_Zexchange : forall {A} `{Ia : Inhabitant A} (L : list A) i j, 0 <= i < Zlength L -> 0 <= j < Zlength L -> Znth i (Zexchange L i j) = Znth j L.
proof: Proof. intros. apply nth_error_Znth; auto. rewrite Zlength_Zexchange. trivial. generalize (Zlength_length _ L (Zlength L)). intro. apply nth_error_exchange; lia. Qed.
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap_model