proposition: Lemma zdrop_inlist_weak : forall (x y : Z) (l : Zlist), inlist Z x (zdrop y l) -> inlist Z x l.
proof: Proof. simple induction l. unfold inlist in |- *. simpl in |- *. intro. assumption. intros h t IH. intros. elim (zeqdec x h). intro. rewrite H0. unfold inlist in |- *. simpl in |- *. left. reflexivity. intro. elim (zeqdec y h). intro. rewrite H1 in H. rewrite zdrop_head_eq in H. apply inlist_tail. assumption. reflexivity. intro. rewrite zdrop_head_neq in H. unfold inlist in H. simpl in H. elim H. intro. elim H0. assumption. intros. apply inlist_tail. apply IH. assumption. assumption. Qed.
imports: Arith ZArith EqNat dec natZ