title: How to easily prove the following in Coq such as using only assumptions?
body: <p>Is there an easy way to prove the following in Coq such as using only assumptions?</p>
  
  <pre><code>(P -&gt; (Q /\ R)) -&gt; (~Q) -&gt; ~P
  </code></pre>