proposition: Lemma nodoubles_drop : forall (p : nat) (l : Zlist) (x : Z), nodoubles p l -> nodoubles p (zdrop x l).
proof: Proof. unfold nodoubles in |- *. intros. apply H. apply zdrop_inlist_weak with x. assumption. apply zdrop_inlist_weak with x. rewrite zdrop_swap. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime