title: How to apply theorems for definitions with restrictions in coq
body: <p>I found a number of examples of definitions with restrictions in coq. Here is for example a variation of the <code>pred</code> function:</p>
  
  <pre><code>Lemma Lemma_NotZeroIsNotEqualToZero : ~ 0 &lt;&gt; 0.
  Proof.
  omega.
  Qed.
  
  Definition pred (s : { n : nat | n &lt;&gt; 0 }) : nat :=
      match s with
          | exist 0 pf =&gt; match (Lemma_NotZeroIsNotEqualToZero pf) with end
          | exist (S n') _ =&gt; n'
      end.
  </code></pre>
  
  <p>But I don't actually understand how to use this definition. Suppose I want to use <code>pred</code> for some natural number and I proved that this number is not zero. Like, for instance, suppose I proved the following lemma:</p>
  
  <pre><code>Lemma Lemma_TenIsNotEqualToZero : 10 &lt;&gt; 0.
  Proof.
  omega.
  Qed.
  </code></pre>
  
  <p>Now, I want to compute what in essence is "<code>pred 10</code>" using <code>Lemma_TenIsNotEqualToZero</code>:</p>
  
  <pre><code>Eval compute in (pred ??).
  </code></pre>
  
  <p>How to do it?</p>