Consequence of $\mathsf{NP\subseteq BPP}$ to $\mathsf{NP\subseteq ZPP}$?

If $\mathsf{NP\subseteq BPP}$, then we know that $\mathsf{NP\subseteq RP}$ (http://www.csie.ntu.edu.tw/~lyuu/complexity/2011/20120103s.pdf). Does $\mathsf{NP\subseteq BPP}$ also imply $\mathsf{NP\subseteq coRP}$ and hence $\mathsf{NP\subseteq BPP}$ also imply $\mathsf{NP\subseteq ZPP}$?

• I believe that's not even known to imply $\: UP\subseteq ZPP \;$. $\;\;\;$ (On the other hand, I also don't know of any oracle relative to which the implication fails.) $\;\;\;\;\;\;\;\;$ – user12859 Aug 22 '15 at 6:31
• @RickyDemer $\mathsf{NP\subseteq BPP\implies NP\subseteq coBPP}$ since $\mathsf{BPP=coBPP}$. Could we switch the arguments in attached proof to yield $\mathsf{NP\subseteq coRP}$? – T.... Aug 22 '15 at 8:23
• No, since it's far from clear that there's any way to efficiently become certain $\hspace{1.76 in}$ of non-membership in an NP language. $\;$ – user12859 Aug 22 '15 at 8:37

If you could prove that implication, then lower bounds such as $NEXP \neq BPP$ would hold unconditionally. (proof: $NEXP = BPP$ implies $NEXP = \Sigma_2 P$ and $NP \subset BPP$, and if the latter also implies $NP$ is in $coRP$ then UNSAT is in $NP$. So $NEXP = \Sigma_2 P = NP$ which is false by the nondeterministic time hierarchy). Good luck!