proposition: Lemma permmod_product : forall (l0 l1 : Zlist) (p : nat), permmod p l0 l1 -> Mod (zproduct l0) (zproduct l1) p.
proof: Proof. simple induction l0. simpl in |- *. intros. rewrite H. simpl in |- *. apply mod_refl. intros h t IH. intros. elim H. intros. elim H0. intros. elim H2. intros. simpl in |- *. rewrite <- zdrop_product with x l1. apply mod_mult_compat. assumption. apply IH. assumption. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime