proposition: Lemma permmod_refl : forall (p : nat) (l : Zlist), permmod p l l.
proof: Proof. simple induction l. simpl in |- *. reflexivity. intros h t IH. split with h. split. apply inlist_head_eq. reflexivity. split. apply mod_refl. rewrite zdrop_head_eq. assumption. reflexivity. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime