title: Is Z.le as defined in the standard library proof irrelevant?
body: <p>In the Coq standard library, there is an enumerated type called <code>comparison</code> with three elements <code>Eq,Lt,Gt</code>.  This is used to define the less-than or less-than-or-equal operators in <code>ZArith</code>: <code>m &lt; n</code> is defined as <code>m ?= n = Lt</code> and <code>m &lt;= n</code> is defined as <code>m ?= n &lt;&gt; Gt</code>.  By virtue of Hedberg's theorem (<code>UIP_dec</code> in the standard library) I can prove that <code>&lt;</code> is proof-irrelevant, but I run into issues when it comes to <code>&lt;=</code>, since it is defined negatively.  I find this particularly annoying, since if <code>&lt;=</code> were defined in the, IMO, more natural way (<code>m ?= n = Lt \/ m ?= n = Eq</code>) I would be able to prove proof-irrelevance just fine.</p>
  
  <p><strong>Context:</strong> I'm using some previously written Coq files where the author uses proof irrelevance as a global axiom to avoid bringing in setoids, and for aesthetic reasons I would prefer to do without axioms.  It seems then to me that my options are:</p>
  
  <ol>
  <li><p>Hope that ultimately <code>Z.le</code> as currently defined is still proof-irrelevant</p></li>
  <li><p>Use my own definition(s) so that proof irrelevance is provable (less satisfying since I'd like to stick to the standard library as much as possible)</p></li>
  <li><p>Rework things with setoids</p></li>
  </ol>