proposition: Lemma zdrop_head_eq : forall (x y : Z) (l : Zlist), x = y -> zdrop x (Cons Z y l) = l.
proof: Proof. simpl in |- *. intros. elim (zeq_bool_eq x y). intros. rewrite H0. reflexivity. assumption. Qed.
imports: Arith ZArith EqNat dec natZ