proposition: Lemma permmod_allex : forall (p : nat) (l0 l1 : Zlist), permmod p l0 l1 -> forall x : Z, inlist Z x l0 -> exists y : Z, inlist Z y l1 /\ Mod x y p /\ permmod p (zdrop x l0) (zdrop y l1).
proof: Proof. simple induction l0. intros. elim H0. intros h0 t0 IH0. intros. elim H. intros h1 Hh1. elim Hh1. intros. elim H2. intros. elim (zeqdec x h0). intro. split with h1. split. assumption. split. rewrite H5. assumption. rewrite zdrop_head_eq. assumption. assumption. intro. elim (IH0 (zdrop h1 l1) H4 x). intros y Hy. elim Hy. intros. elim H7. intros. split with y. split. apply zdrop_inlist_weak with h1. assumption. split. assumption. rewrite zdrop_head_neq. split with h1. split. elim (zeqdec h1 y). intro. rewrite H10 in H6. rewrite H10. assumption. intro. apply zdrop_neq_inlist. assumption. assumption. split. assumption. rewrite zdrop_swap. assumption. assumption. elim (inlist_head_neq Z x h0 t0). intros. apply H6. assumption. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime