proposition: Lemma until_pos : forall (n : nat) (x : Z), inlist Z x (until n) -> (0 < x)%Z.
proof: Proof. simple induction n. unfold inlist in |- *. simpl in |- *. intros. elim H. intros m IH. intros. unfold inlist in H. simpl in H. elim H. intros. rewrite H0. unfold Z.lt in |- *. simpl in |- *. reflexivity. intros. apply IH. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime