proposition: Lemma Zexchange_symm {A}: forall (L : list A) i j, 0 <= i < Zlength L -> 0 <= j < Zlength L -> Zexchange L i j = Zexchange L j i.
proof: Proof. intros. rewrite Zlength_correct in H, H0. apply exchange_symm; lia. Qed.
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap_model