proposition: Lemma permmod_drop_drop : forall (p : nat) (x y : Z) (l : Zlist), Mod x y p -> inlist Z x l -> inlist Z y l -> permmod p (zdrop x l) (zdrop y l).
proof: Proof. intros. apply permmod_drop_drop1 with (length Z l). reflexivity. assumption. assumption. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime