proposition: Lemma Zexchange_Permutation: forall A (L : list A) i j, Permutation L (Zexchange L i j).
proof: Proof. intros. unfold Zexchange. symmetry. apply exchange_Permutation. Qed.
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap_model