proposition: Lemma until_not_0mod : forall (p : nat) (x : Z), 0 < p -> inlist Z x (until (pred p)) -> ~ Mod x 0 p.
proof: Proof. intros. apply mod_repr_non_0. split. apply (until_pos (pred p) x). assumption. rewrite (S_pred p 0). rewrite Znat.inj_S. apply Zle_lt_succ. apply until_le_n. assumption. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime