title: Why does `ev n (S(S n))' decrease the number and not increase it?
body: <p>I was going through the <a href="https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html" rel="nofollow noreferrer">software foundations course</a> and saw the following simple code:</p>
  
  <pre><code>Inductive ev : nat -&gt; Prop :=
  | ev_0 : ev 0
  | ev_SS : forall n : nat, ev n -&gt; ev (S (S n)).
  </code></pre>
  
  <p>however, when the use the <code>apply ev_SS.</code> tactic on a proof that <code>ev 4</code> is true:</p>
  
  <pre><code>Theorem ev_4 : ev 4.
  Proof.  (* goal: ev 4*)
    apply ev_SS. (* goal changed to: ev 2, why??? *)
    apply ev_SS. 
    apply ev_0. 
  Qed.
  </code></pre>
  
  <p>the application of <code>ev_SS.</code> confuses me. If I plugged in a number to the "inference rule" I'd get it's increasing not decreasing:</p>
  
  <pre><code>ev 2 == ev 2 -&gt; ev (S (S 2)).
  </code></pre>
  
  <p>what am I misunderstanding?</p>
  
  <hr>
  
  <p>Similarly, whats going on here:</p>
  
  <pre><code>Theorem ev_4' : ev 4.
  Proof. 
    apply (ev_SS 2 (ev_SS 0 ev_0)). 
  Qed.
  </code></pre>
  
  <p>Is there a better way in general to explore how transformations happen from one place to another in Coq? If I could do that I could inspect more clearly how things happen in the prover and why.</p>