proposition: Lemma zdrop_neq_inlist : forall (x y : Z) (l : Zlist), x <> y -> inlist Z x l -> inlist Z x (zdrop y l).
proof: Proof. simple induction l. intros. elim H0. intros h t IH. intros. elim (zeqdec x h). intro. rewrite zdrop_head_neq. apply inlist_head_eq. assumption. rewrite <- H1. intro. apply H. symmetry in |- *. assumption. intro. elim (zeqdec y h). intro. rewrite zdrop_head_eq. elim (inlist_head_neq Z x h t). intros. apply H3. assumption. assumption. assumption. intro. rewrite zdrop_head_neq. elim (inlist_head_neq Z x h (zdrop y t)). intros. apply H4. apply IH. assumption. elim (inlist_head_neq Z x h t). intros. apply H5. assumption. assumption. assumption. assumption. Qed.
imports: Arith ZArith EqNat dec natZ