proposition: Lemma allex_permmod : forall (p : nat) (l0 l1 : Zlist), length Z l0 = length Z l1 -> (forall x0 : Z, inlist Z x0 l0 -> exists x1 : Z, inlist Z x1 l1 /\ Mod x0 x1 p /\ permmod p (zdrop x0 l0) (zdrop x1 l1)) -> permmod p l0 l1.
proof: Proof. simple induction l0. simple induction l1. intros. apply permmod_nil. intros. discriminate H0. intros h0 t0 IH0. intros. elim (H0 h0). intro x1. intros. elim H1. intros. elim H3. intros. rewrite zdrop_head_eq in H5. apply permmod_drop_cons with x1. assumption. assumption. assumption. reflexivity. apply inlist_head_eq. reflexivity. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime