proposition: Lemma ZallLinCombMod_ok : forall (a n m N : Z) (qlist : Zlist), ZallLinCombMod a n m N qlist -> forall qi : Z, inlist Z qi qlist -> ZLinCombMod 1 (ZExp a (m * zmultDrop qi qlist) - 1) n N.
proof: Proof. intros. elim (alllist_ok Z (fun q : Z => ZLinCombMod 1 (ZExp a (m * zmultDrop q qlist) - 1) n N) qlist). intros. apply H1. assumption. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo gcd modprime order