title: Type coercion from nat to rat
body: <p>I'm stuck with this very simple lemma, and wonder what is the best way to proceed.</p>
  <pre><code>From mathcomp Require Import ssrint rat ssralg ssrnum.
  
  Import GRing.Theory.
  Import Num.Theory.
  Import Num.Def.
  
  Open Scope ring_scope.
  
  Lemma X (n m : nat) : (n &lt;= m)%N -&gt; n%:Q &lt;= m%:Q.
  Proof.
  rewrite -lez_nat.
  </code></pre>