proposition: Lemma nat_inc_list_plus_1_Permutation: forall (i : Z), 0 <= i -> Permutation (nat_inc_list (Z.to_nat (i + 1))) (i :: nat_inc_list (Z.to_nat i)).
proof: Proof. intros. replace (Z.to_nat (i + 1)) with (1 + Z.to_nat i)%nat by lia. simpl. symmetry. rewrite Z2Nat.id; auto. apply Permutation_cons_append. Qed.
imports: RelationClasses VST.floyd.proofauto CertiGraph.lib.List_ext CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.binary_heap_malloc_spec CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel