proposition: Lemma Znth_nth_error {A} `{Ia : Inhabitant A} : forall (L : list A) (i : Z), 0 <= i < Zlength L -> nth_error L (Z.to_nat i) = Some (Znth i L).
proof: Proof. intros. rewrite <- nth_Znth; trivial. apply nth_error_nth. rewrite <- ZtoNat_Zlength. lia. Qed.
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap_model