proposition: Lemma untiln_prod_not_0modp : forall p n : nat, 0 < n -> n < p -> Prime p -> ~ Mod (zproduct (until n)) 0 p.
proof: Proof. simple induction n. intro. elim (lt_irrefl 0). assumption. intros m IH H0m Hmp Hp. change (~ Mod (Z_of_nat (S m) * zproduct (until m)) 0 p) in |- *. intro. elim (mod_mult_0 p (Z_of_nat (S m)) (zproduct (until m))). intro. elim (mod_repr_non_0 p (Z_of_nat (S m))). split. change (Z_of_nat 0 < Z_of_nat (S m))%Z in |- *. apply Znat.inj_lt. assumption. apply Znat.inj_lt. assumption. assumption. intro. elim (le_lt_or_eq 0 m). intro. elim IH. assumption. apply lt_trans with (S m). apply lt_n_Sn. assumption. assumption. assumption. intro. rewrite <- H1 in H. simpl in H. elim mod_0not1 with p. elim Hp. intros. assumption. apply mod_sym. assumption. apply le_O_n. assumption. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime