proposition: Lemma Zexchange_head_foot: forall A (head : A) body foot, Zexchange ((head :: body) ++ [foot]) 0 (Zlength (head :: body)) = ((foot :: body) ++ [head]).
proof: Proof. intros. unfold Zexchange. simpl. rewrite Zlength_correct. rewrite Nat2Z.id. do 2 rewrite app_comm_cons. apply exchange_head_foot. Qed.
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap_model