proposition: Lemma nodoubles_allex_permmod1 : forall (n p : nat) (l0 l1 : Zlist), n = length Z l0 -> n = length Z l1 -> Prime p -> length Z l0 = length Z l1 -> nodoubles p l0 -> allex p l0 l1 -> permmod p l0 l1.
proof: Proof. simple induction n. intros. rewrite length_0 with Z l0. rewrite length_0 with Z l1. apply permmod_nil. symmetry in |- *. assumption. symmetry in |- *. assumption. intros m IH. intros. apply allex_permmod. assumption. intros x Hx. elim H4 with x. intros y Hy. elim Hy. intros. split with y. split. assumption. split. assumption. apply IH. apply S_inj. rewrite zdrop_length. assumption. assumption. apply S_inj. rewrite zdrop_length. assumption. assumption. assumption. apply S_inj. rewrite zdrop_length. rewrite zdrop_length. assumption. assumption. assumption. apply nodoubles_drop. assumption. apply allex_nodoubles_drop. assumption. assumption. assumption. assumption. assumption. assumption. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime