proposition: Lemma permmod_sym : forall (p : nat) (l1 l2 : Zlist), permmod p l1 l2 -> permmod p l2 l1.
proof: Proof. simple induction l1. simpl in |- *. intros. rewrite H. apply permmod_nil. intros h1 t1 IH1. intros. elim H. intros y Hy. elim Hy. intros. elim H1. intros. apply permmod_drop with y h1. apply mod_sym. assumption. assumption. apply inlist_head_eq. reflexivity. rewrite zdrop_head_eq. apply IH1. assumption. reflexivity. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime