[ true \Rightarrow prime (S(S m1))
| false \Rightarrow \lnot (prime (S(S m1)))].
apply (eqb_elim (smallest_factor (S(S m1))) (S(S m1))).
[ true \Rightarrow prime (S(S m1))
| false \Rightarrow \lnot (prime (S(S m1)))].
apply (eqb_elim (smallest_factor (S(S m1))) (S(S m1))).