proposition: Lemma until_mod_all : forall (p : nat) (x : Z), 0 < p -> ~ Mod x 0 p -> exists y : Z, inlist Z y (until (pred p)) /\ Mod x y p.
proof: Proof. intros. elim (zdiv_rem (Z_of_nat p) x). intro q. intros. elim H1. intro r. intros. elim H2. intros. elim H3. intros. elim (Zle_lt_or_eq 0 r). intro. split with r. split. apply until_ok. split. assumption. apply Zlt_succ_le. rewrite <- Znat.inj_S. rewrite <- (S_pred p 0). assumption. assumption. split with q. rewrite Zplus_comm. rewrite Zmult_comm. assumption. intro. elim H0. split with q. rewrite H7. rewrite Zplus_comm. rewrite Zmult_comm. assumption. assumption. change (Z_of_nat p > Z_of_nat 0)%Z in |- *. apply Znat.inj_gt. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime