proposition: Lemma Zlength_correct l : Zlength l = Z.of_nat (length l).
proof: Proof. assert (H : forall l acc, Zlength_aux acc A l = acc + Z.of_nat (length l)). - clear l. intros l; induction l as [|? ? IHl]. + auto with zarith. + intros. simpl length; simpl Zlength_aux. rewrite IHl, Nat2Z.inj_succ, Z.add_succ_comm; auto. - unfold Zlength. now rewrite H. Qed.
imports: ZArithRing ZArith_base Wf_nat List