proposition: Lemma until_nodoubles : forall p : nat, Prime p -> nodoubles p (until (pred p)).
proof: Proof. intros. apply until_nodoubles1. assumption. apply lt_pred_n_n. apply lt_trans with 1. apply lt_n_Sn. elim H. intros. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime