proposition: Lemma permmod_trans1 : forall (n p : nat) (l0 l1 l2 : Zlist), length Z l0 = n -> length Z l1 = n -> length Z l2 = n -> permmod p l0 l1 -> permmod p l1 l2 -> permmod p l0 l2.
proof: Proof. simple induction n. intros. rewrite length_0 with Z l0. rewrite length_0 with Z l2. apply permmod_nil. assumption. assumption. intros m IH. intros p l0 l1 l2 Hl0 Hl1 Hl2 H01 H12. apply allex_permmod. transitivity (length Z l1). apply permmod_length with p. assumption. apply permmod_length with p. assumption. intros x0 Hx0. elim (permmod_allex p l0 l1 H01 x0). intros x1 H0. elim H0. intros Hx1 H1. elim H1. intros Hm01 Hd01. elim (permmod_allex p l1 l2 H12 x1). intros x2 H2. elim H2. intros Hx2 H3. elim H3. intros Hm12 Hd12. split with x2. split. assumption. split. apply mod_trans with x1. assumption. assumption. apply IH with (zdrop x1 l1). apply S_inj. rewrite zdrop_length. assumption. assumption. apply S_inj. rewrite zdrop_length. assumption. assumption. apply S_inj. rewrite zdrop_length. assumption. assumption. assumption. assumption. assumption. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime