proposition: Lemma permmod_length : forall (p : nat) (l1 l2 : Zlist), permmod p l1 l2 -> length Z l1 = length Z l2.
proof: Proof. simple induction l1. simpl in |- *. intros. rewrite H. simpl in |- *. reflexivity. intros h t IH. simpl in |- *. intros. elim H. intros y Hy. elim Hy. intros. elim H1. intros. rewrite (IH (zdrop y l2)). rewrite zdrop_length with y l2. reflexivity. assumption. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime