proposition: Lemma nodoubles_allex_permmod : forall (p : nat) (l0 l1 : Zlist), Prime p -> length Z l0 = length Z l1 -> nodoubles p l0 -> allex p l0 l1 -> permmod p l0 l1.
proof: Proof. intros. apply nodoubles_allex_permmod1 with (length Z l0). reflexivity. assumption. assumption. assumption. assumption. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime