fact: Definition allLinCombMod (a : Z) (n m : nat) (qlist : natlist) := alllist nat (fun q : nat => LinCombMod 1 (Exp a (m * multDrop q qlist) - 1) (Z_of_nat n) n) qlist.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo gcd modprime order