proposition: Lemma permmod_cons_extend : forall (p : nat) (x1 x2 : Z) (l1 l2 : Zlist), permmod p l1 l2 -> Mod x1 x2 p -> permmod p (Cons Z x1 l1) (Cons Z x2 l2).
proof: Proof. intros. apply permmod_drop with x1 x2. assumption. apply inlist_head_eq. reflexivity. apply inlist_head_eq. reflexivity. rewrite zdrop_head_eq. rewrite zdrop_head_eq. assumption. reflexivity. reflexivity. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime