proposition: Lemma permmod_drop : forall (p : nat) (x1 x2 : Z) (l1 l2 : Zlist), Mod x1 x2 p -> inlist Z x1 l1 -> inlist Z x2 l2 -> permmod p (zdrop x1 l1) (zdrop x2 l2) -> permmod p l1 l2.
proof: Proof. simple induction l1. simpl in |- *. intros. elim H0. intros h t IH. intros l2 Hm. elim (zeqdec x1 h). intros. simpl in |- *. split with x2. split. assumption. split. rewrite <- H. assumption. rewrite H in H2. rewrite zdrop_head_eq in H2. assumption. reflexivity. intro. rewrite zdrop_head_neq. intros. elim H2. intros y Hy. elim Hy. intros. elim H4. intros. split with y. split. apply zdrop_inlist_weak with x2. assumption. split. assumption. rewrite zdrop_swap in H6. apply IH. assumption. elim (inlist_head_neq Z x1 h t). intros. apply H7. assumption. assumption. elim (zeqdec x2 y). intro. rewrite H7. rewrite H7 in H3. assumption. intro. apply zdrop_neq_inlist. assumption. assumption. assumption. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime