title: Coq : Admit assert
body: <p>Is there a way to admit asserts in Coq ?</p>
  
  <p>Suppose I have a theorem like this:</p>
  
  <pre><code>Theorem test : forall m n : nat,
      m * n = n * m.
  Proof.
    intros n m.
    assert (H1: m + m * n = m * S n). { Admitted. }
  Abort.
  </code></pre>
  
  <p>The above assert doesn't seem to work for me.</p>
  
  <p>The error I receive is:</p>
  
  <pre><code>Error: No focused proof (No proof-editing in progress).
  </code></pre>
  
  <p>What I want is something like <code>undefined</code> in Haskell. Baiscally, I will come back to this later and prove it. Is there something like that in Coq to achieve it ?</p>