proposition: Lemma nodoubles_ind : forall (p : nat) (h : Z) (t : Zlist), (forall x : Z, inlist Z x t -> ~ Mod h x p) -> nodoubles p t -> nodoubles p (Cons Z h t).
proof: Proof. intros. unfold nodoubles in |- *. intros. elim (zeqdec x h). intro. rewrite zdrop_head_eq in H2. rewrite H3. apply (H y). assumption. assumption. intro. rewrite zdrop_head_neq in H2. elim (zeqdec y h). intro. rewrite H4. intro. elim (H x). elim (inlist_head_neq Z x h t). intros. apply H6. assumption. assumption. apply mod_sym. assumption. intro. unfold nodoubles in H0. apply (H0 x). elim (inlist_head_neq Z x h t). intros. apply H5. assumption. assumption. elim (inlist_head_neq Z y h (zdrop x t)). intros. apply H5. assumption. assumption. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime