title: Introduce previously proved theorem as hypothesis
body: <p>Suppose that I have already proved some theorem in coq, and later I want to introduce it as a hypothesis in the proof of another theorem. Is there a succinct way to do this?</p>
  
  <p>The need for this typically arises for me when I want to do something like a proof by cases. And I've discovered that one way to do this is to <code>assert</code> the statement of the theorem, and then immediately prove it, but this seems kind of cumbersome. For example I tend to write things like:</p>
  
  <pre><code>Require Import Arith.EqNat.
  
  Definition Decide P := P \/ ~P.
  
  Theorem decide_eq_nat: forall x y: nat, Decide (x = y).
  Proof.
    intros x y. remember (beq_nat x y) as b eqn:E. destruct b.
      left. apply beq_nat_eq. assumption.
      right. apply beq_nat_false. symmetry. assumption. Qed.
  
  Theorem silly: forall x y: nat, x = y \/ x &lt;&gt; y.
  Proof.
    intros x y.
    assert (Decide (x = y)) as [E|N] by apply decide_eq_nat.
      left. assumption.
      right. assumption. Qed.
  </code></pre>
  
  <p>But is there an easier way than having to type the whole <code>assert [statement] by apply [theorem]</code> thing?</p>