I'm looking for a problem that (provably) lies in NP, but for which the proof that it lies in NP is "not completely trivial/obvious". Anyone know of such a problem (ideally a "natural" problem)?
I think primality is a good candidate for this:
Witnessing that a number is composite is easy (give a factorization), and it can be checked efficiently.
Witnessing that a number is prime is not so obvious. But it has been known since the 80s that this can be done. So for a long time, PRIMES was a natural language in "NP intersect coNP".
It is known since like 2004 that PRIMES is actually in P