apply le_S_S_to_le.rewrite < S_pred.
unfold prime in H.elim H.assumption.assumption.
unfold prime in H.elim H.apply (trans_lt ? (S O)).
apply le_S_S_to_le.rewrite < S_pred.
unfold prime in H.elim H.assumption.assumption.
unfold prime in H.elim H.apply (trans_lt ? (S O)).