[Tex/LaTex] Including both equation numbering and remarks in align environment

Question

I'm trying to write sequent proofs with aligned formulae in the center, equation numbers aligned left, and remarks aligned right. Example of what I want below:

But from what I've seen around StackExchange, tags on a line of an alignment replace the numbering of that line, as well as share the same alignment setting. Here's a sample of what I'm having trouble with.

\documentclass[leqno]{article}
\usepackage{amsmath}
\usepackage{amsthm}
\begin{document}
 \begin{align}
  Rab 
  &\implies Rab                                \tag{R0}
  \\ &\implies Rab,\neg Rab                    \tag{R2a}
  \\ &\implies Rab, \exists y \neg Ray   
  \\ \neg \exists y \neg Ray 
  &\implies Rab   
  \\ \forall y Ray 
  &\implies Rab      
  \\ \exists x \forall y Rxy 
  &\implies Rab   
  \\ \exists x \forall y Rxy 
  &\implies \exists x Rxb
  \\ \exists x \forall y Rxy, \neg \exists x Rxb 
  &\implies 
  \\ \exists x \forall y Rxy, \exists y \neg \exists x Rxy 
  &\implies 
  \\ \exists x \forall y Rxy 
  &\implies \neg \exists y \neg \exists x Rxy 
  \\ \exists x \forall y Rxy 
  &\implies \forall y \exists x Rxy \qedhere
 \end{align}
\end{document}

An image of the corresponding output:

Answer 1

Only the first 3 lines modified, but the rest should be easy. Alas, more ampersands needed.

\documentclass[leqno]{article}
\usepackage{amsmath}
\usepackage{amsthm}
\begin{document}
 \begin{align}
  Rab 
  &\implies Rab                                &\text{(RO)}&
  \\ &\implies Rab,\neg Rab            &        \text{(R2aa)}&
  \\ &\implies Rab, \exists y \neg Ray  & \text{(and so on)}& 
  \\ \neg \exists y \neg Ray 
  &\implies Rab   
  \\ \forall y Ray 
  &\implies Rab      
  \\ \exists x \forall y Rxy 
  &\implies Rab   
  \\ \exists x \forall y Rxy 
  &\implies \exists x Rxb
  \\ \exists x \forall y Rxy, \neg \exists x Rxb 
  &\implies 
  \\ \exists x \forall y Rxy, \exists y \neg \exists x Rxy 
  &\implies 
  \\ \exists x \forall y Rxy 
  &\implies \neg \exists y \neg \exists x Rxy 
  \\ \exists x \forall y Rxy 
  &\implies \forall y \exists x Rxy \qedhere
 \end{align}
\end{document}