proposition: Lemma permmod_drop_cons : forall (p : nat) (x1 x2 : Z) (t1 l2 : Zlist), Mod x1 x2 p -> inlist Z x2 l2 -> permmod p t1 (zdrop x2 l2) -> permmod p (Cons Z x1 t1) l2.
proof: Proof. intros. apply permmod_drop with x1 x2. assumption. apply inlist_head_eq. reflexivity. assumption. rewrite zdrop_head_eq. assumption. reflexivity. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime