proposition: Lemma Zlength_Zexchange {A : Type} : forall (L : list A) i j, Zlength (Zexchange L i j) = Zlength L.
proof: Proof. intros. unfold Zexchange. do 2 rewrite Zlength_correct. rewrite exchange_length. trivial. Qed.
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap_model