proposition: Lemma until_nodoubles1 : forall p : nat, Prime p -> forall n : nat, n < p -> nodoubles p (until n).
proof: Proof. simple induction n. intros. simpl in |- *. apply nodoubles_nil. intros m IH Hb. change (nodoubles p (Cons Z (Z_of_nat (S m)) (until m))) in |- *. apply nodoubles_ind. intros. intro. elim (Zlt_not_le x (Z_of_nat (S m))). rewrite Znat.inj_S. apply Zle_lt_succ. apply until_le_n. assumption. apply Zeq_le. apply mod_repr_eq with p. elim H. intros. apply lt_trans with 1. apply lt_n_Sn. assumption. split. change (Z_of_nat 0 < Z_of_nat (S m))%Z in |- *. apply Znat.inj_lt. apply lt_O_Sn. apply Znat.inj_lt. assumption. split. apply until_pos with m. assumption. apply Z.le_lt_trans with (Z_of_nat m). apply until_le_n. assumption. apply Znat.inj_lt. apply le_lt_trans with (S m). apply le_n_Sn. assumption. assumption. apply IH. apply le_lt_trans with (S m). apply le_n_Sn. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime