title: Coq Real numbers -lexing and parsing 3.14
body: <p>With Reals library imported</p>
  
  <pre><code>Require Import Reals.
  </code></pre>
  
  <p>How can I define constants such as 3.14 or 10.1 and use them for function definition or computation ?</p>