Proof of posint_atom_imp_prime