title: Prop and bool in Coq
body: <p>How can I use a comparison of to rational numbers in an if-statement?</p>
  
  <pre><code>if 1 = 2 then 1 else 2
  </code></pre>
  
  <p><code>1 = 2</code> is of course <code>Prop</code> and not <code>bool</code>.</p>