proposition: Lemma zdrop_length : forall (x : Z) (l : Zlist), inlist Z x l -> S (length Z (zdrop x l)) = length Z l.
proof: Proof. simple induction l. unfold inlist in |- *. simpl in |- *. intros. elim H. intros h t IH. intros. elim (zeqdec x h). intro. simpl in |- *. elim (zeq_bool_eq x h). intros. rewrite H1. reflexivity. assumption. intro. simpl in |- *. elim (zeq_bool_neq x h). intros. rewrite H1. simpl in |- *. rewrite IH. reflexivity. elim H. intros. elim H0. assumption. intros. assumption. assumption. Qed.
imports: Arith ZArith EqNat dec natZ