proposition: Lemma permmod_drop_drop1 : forall (n p : nat) (x y : Z) (l : Zlist), n = length Z l -> Mod x y p -> inlist Z x l -> inlist Z y l -> permmod p (zdrop x l) (zdrop y l).
proof: Proof. simple induction n. intros. rewrite length_0 with Z l. simpl in |- *. reflexivity. symmetry in |- *. assumption. intros m IH. intros. elim (zeqdec x y). intro. rewrite H3. apply permmod_refl. intro. apply allex_permmod. apply S_inj. rewrite zdrop_length. rewrite zdrop_length. reflexivity. assumption. assumption. intros z Hz. elim (zeqdec y z). intro. split with x. split. apply zdrop_neq_inlist. assumption. assumption. split. rewrite <- H4. apply mod_sym. assumption. rewrite H4. rewrite zdrop_swap. apply permmod_refl. intro. split with z. split. apply zdrop_neq_inlist. intro. apply H4. symmetry in |- *. assumption. apply zdrop_inlist_weak with x. assumption. split. apply mod_refl. rewrite (zdrop_swap z). rewrite (zdrop_swap z). apply (IH p x y (zdrop z l)). apply S_inj. rewrite zdrop_length. assumption. apply zdrop_inlist_weak with x. assumption. assumption. apply zdrop_inlist_swap. assumption. assumption. apply zdrop_neq_inlist. assumption. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime