proposition: Lemma prime_2: prime 2.
proof: Proof. apply prime_intro. - red; auto. - intros n (H,H'); Z.le_elim H; auto with zarith. + contradict H'; auto with zarith. now apply Zle_not_lt, (Zlt_le_succ 1). + subst n. constructor; auto with zarith. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat