proposition: Lemma prime2 : Prime 2.
proof: Proof. apply primepropdiv. auto. intro q. case q. intros. elim H. intro. elim (lt_n_O 1). assumption. intro q1. case q1. intros. elim H. intro. elim (lt_irrefl 1). assumption. intro q2. case q2. simpl in |- *. intros. auto. intro q3. simpl in |- *. intros. repeat apply gt_n_S. apply gt_Sn_O. Qed.
imports: ZArith Wf_nat lemmas natZ dec divides modulo list