proposition: Lemma allLinCombMod_ok : forall (a : Z) (n m : nat) (qlist : natlist), allLinCombMod a n m qlist <-> (forall qi : nat, inlist nat qi qlist -> LinCombMod 1 (Exp a (m * multDrop qi qlist) - 1) (Z_of_nat n) n).
proof: Proof. intros. elim (alllist_ok nat (fun q : nat => LinCombMod 1 (Exp a (m * multDrop q qlist) - 1) (Z_of_nat n) n) qlist). split. intros. apply H. assumption. assumption. intros. apply H0. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo gcd modprime order