fact: Definition nodoubles (p : nat) (l : Zlist) : Prop := forall x : Z, inlist Z x l -> forall y : Z, inlist Z y (zdrop x l) -> ~ Mod x y p.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime