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