title: Best way to handle (sub) types of the form `{ x : nat | x >= 13 /\ x <= 19 }`?
body: <p><strong>Coq</strong> would let me define this :</p>
  
  <pre><code>Definition teenagers : Set := { x : nat | x &gt;= 13 /\ x &lt;= 19 }.
  </code></pre>
  
  <p>and also :</p>
  
  <pre><code>Variable Julia:teenagers.
  </code></pre>
  
  <p>but not :</p>
  
  <pre><code>Example minus_20 : forall x:teenagers, x&lt;20.
  </code></pre>
  
  <p>or :</p>
  
  <pre><code>Example Julia_fact1 : Julia &gt; 12.
  </code></pre>
  
  <p>This is because Julia (of type <em>teenagers</em>) cannot be compared to 12 (<em>nat</em>).</p>
  
  <p><strong>Q:</strong> How should I inform Coq that Julia's support type is <em>nat</em> so that I can write anything useful about her ?</p>
  
  <p><strong>Q':</strong> My definition of teenagers seems like a dead end ; it is more declarative than constructive and I seem to have lost inductive properties of <em>nat</em>. How can I show up its inhabitants ? If there is no way, I can still stick to <em>nat</em> and work with <em>Prop</em> and functions. (newbie here, less than one week self learning with <a href="https://www.cis.upenn.edu/~bcpierce/sf/current/index.html" rel="nofollow">Pierce's SF</a>).</p>