proposition: Lemma permmod_trans : forall (p : nat) (l0 l1 l2 : Zlist), permmod p l0 l1 -> permmod p l1 l2 -> permmod p l0 l2.
proof: Proof. intros. apply permmod_trans1 with (length Z l0) l1. reflexivity. symmetry in |- *. apply permmod_length with p. assumption. symmetry in |- *. transitivity (length Z l1). apply permmod_length with p. assumption. apply permmod_length with p. assumption. assumption. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime