proposition: Lemma until_ok : forall (n : nat) (x : Z), (0 < x <= Z_of_nat n)%Z -> inlist Z x (until n).
proof: Proof. simple induction n. simpl in |- *. intros. elim H. intros. elim (Zle_not_lt x 0). assumption. assumption. intros m IH. intros. elim H. intros. elim (Zle_lt_or_eq x (Z_of_nat (S m))). intros. unfold inlist in |- *. simpl in |- *. right. unfold inlist in IH. apply IH. split. assumption. apply Zlt_succ_le. rewrite <- Znat.inj_S. assumption. intro. rewrite H2. unfold inlist in |- *. simpl in |- *. left. reflexivity. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime