title: Coq nat type check on match
body: <pre><code>Theorem nzgtz : ~ 0 &gt; 0.
  Proof.
  unfold not.
  unfold gt.
  unfold lt.
  intros H.
  inversion H.
  Qed.
  
  Print nzgtz.
  
  Definition pred1 (n : nat) : n &gt; 0 -&gt; nat :=
    match n with
   | O =&gt; fun pf =&gt; match (nzgtz pf) with end
   | S n' =&gt; fun _ =&gt; n'
   end.
  </code></pre>
  
  <p>I am confused about how the first branch with the <code>O</code> returns a function with type <code>(0 &gt; 0) -&gt; nat</code>. The question is: how is <code>match False with end</code> a <code>nat</code>? It seems that no value is returned?! What does that expression mean?</p>