proposition: Lemma until_prod_not_0mod : forall p : nat, Prime p -> ~ Mod (zproduct (until (pred p))) 0 p.
proof: Proof. intros. elim H. intros. apply untiln_prod_not_0modp; auto with arith. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime