proposition: Theorem prime_3: prime 3.
proof: Proof. apply prime_intro; auto with zarith. - red; auto. - intros n (H,H'); Z.le_elim H; auto with zarith. + replace n with 2. * constructor; auto with zarith. intros x (q,Hq) (q',Hq'). exists (q' - q). ring_simplify. now rewrite <- Hq, <- Hq'. * apply Z.le_antisymm. ++ now apply (Zlt_le_succ 1). ++ now apply (Z.lt_le_pred _ 3). + replace n with 1 by trivial. constructor; auto with zarith. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat