proposition: Lemma permmod_drop_rev : forall (p : nat) (l0 l1 : Zlist) (x0 x1 : Z), Mod x0 x1 p -> inlist Z x0 l0 -> inlist Z x1 l1 -> permmod p l0 l1 -> permmod p (zdrop x0 l0) (zdrop x1 l1).
proof: Proof. intros. elim (permmod_allex p l0 l1 H2 x0). intros y Hy. elim Hy. intros. elim H4. intros. apply permmod_trans with (zdrop y l1). assumption. apply permmod_drop_drop. apply mod_trans with x0. apply mod_sym. assumption. assumption. assumption. assumption. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime