1 files changed, 12 insertions, 1 deletions
diff --git a/kvx/lib/IterList.v b/kvx/lib/IterList.v
index b9eb5922..49beb1c5 100644
--- a/kvx/lib/IterList.v
+++ b/kvx/lib/IterList.v
@@ -82,4 +82,15 @@ Proof.
   destruct (le_lt_dec n (List.length l)); try omega.
   intros; exploit (iter_tail_inject1 n (length l) l); try omega.
   rewrite iter_tail_reach_nil. auto.
-Qed.
-\ No newline at end of file
+Qed.
+
+Lemma list_length_z_nat (A: Type) (l: list A): list_length_z l = Z.of_nat (length l).
+Proof.
+  induction l; auto.
+  rewrite list_length_z_cons. simpl. rewrite Zpos_P_of_succ_nat. omega.
+Qed.
+
+Lemma list_length_nat_z (A: Type) (l: list A): length l = Z.to_nat (list_length_z l).
+Proof.
+  intros; rewrite list_length_z_nat, Nat2Z.id. auto.
+Qed.