proposition: Lemma allex_nodoubles_drop : forall (p : nat) (l0 l1 : Zlist) (x0 x1 : Z), Prime p -> Mod x0 x1 p -> inlist Z x0 l0 -> inlist Z x1 l1 -> nodoubles p l0 -> allex p l0 l1 -> allex p (zdrop x0 l0) (zdrop x1 l1).
proof: Proof. intros. unfold allex in |- *. intros x Hx. elim (H4 x). intros y Hy. elim Hy. intros. split with y. split. apply zdrop_neq_inlist. intro. rewrite H7 in H6. elim H3 with x x0. apply zdrop_inlist_weak with x0. assumption. apply zdrop_inlist_swap. assumption. assumption. apply mod_trans with x1. assumption. apply mod_sym. assumption. assumption. assumption. apply zdrop_inlist_weak with x0. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime