proposition: Lemma zdrop_swap : forall (x y : Z) (l : Zlist), zdrop x (zdrop y l) = zdrop y (zdrop x l).
proof: Proof. simple induction l. simpl in |- *. reflexivity. intros h t IH. elim (zeqdec x h). elim (zeqdec y h). intros. rewrite H. rewrite H0. reflexivity. intros. rewrite (zdrop_head_eq x h t). rewrite (zdrop_head_neq y h t). rewrite zdrop_head_eq. reflexivity. assumption. assumption. assumption. elim (zeqdec y h). intros. rewrite (zdrop_head_eq y h). rewrite (zdrop_head_neq x h). rewrite zdrop_head_eq. reflexivity. assumption. assumption. assumption. intros. rewrite (zdrop_head_neq y h). rewrite (zdrop_head_neq x h). rewrite (zdrop_head_neq x h). rewrite (zdrop_head_neq y h). rewrite IH. reflexivity. assumption. assumption. assumption. assumption. Qed.
imports: Arith ZArith EqNat dec natZ