proposition: Lemma until_le_n : forall (n : nat) (x : Z), inlist Z x (until n) -> (x <= Z_of_nat n)%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. apply Z.le_refl. intros. apply Z.le_trans with (Z_of_nat m). apply IH. assumption. apply Znat.inj_le. apply le_S. apply le_n. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime