title: How to "flip" an equality proposition in Coq?
body: <p>If I'm in Coq and I find myself in a situation with a goal like so:</p>
  
  <pre><code>==================
    x = y -&gt; y = x
  </code></pre>
  
  <p>Is there a tactic that can can take care of this in one swoop? As it is, I'm writing</p>
  
  <pre><code>intros H. rewrite -&gt; H. reflexivity.
  </code></pre>
  
  <p>But it's a bit clunky.</p>