title: How to repeat proof tactics in case in Coq?
body: <p>I would like to extend the exercise 6.10 in Coq'Art by adding a theorem that forall months which are not January, is_January will equal false.</p>
  
  <p>My definition of months looks like this:</p>
  
  <pre><code> Inductive month : Set :=
     | January : month
     | February : month
     | March : month
     | April : month
     | May : month
     | June : month
     | July : month
     | August : month
     | September : month
     | October : month
     | November : month
     | December : month
    .
  
  Check month_rect.
  </code></pre>
  
  <p>My definition of is_January looks like this:</p>
  
  <pre><code>Definition is_January (m : month) : Prop :=
    match m with
    | January =&gt; True
    | other   =&gt; False
    end.
  </code></pre>
  
  <p>I am doing the following to test that it is correct.</p>
  
  <pre><code>Eval compute in (is_January January).
  Eval compute in (is_January December).
  
  Theorem is_January_eq_January :
    forall m : month, m = January -&gt; is_January m = True.
  Proof.
    intros m H.
    rewrite H.
    compute; reflexivity.
  Qed.
  </code></pre>
  
  <p>I am not very happy with this theorem's proof.</p>
  
  <pre><code>Theorem is_January_neq_not_January :
    forall m : month, m &lt;&gt; January -&gt; is_January m = False.
  Proof.
    induction m.
    - contradiction.
    - intro H; simpl; reflexivity.
    - intro H; simpl; reflexivity.
    - intro H; simpl; reflexivity.
    - intro H; simpl; reflexivity.
    - intro H; simpl; reflexivity.
    - intro H; simpl; reflexivity.
    - intro H; simpl; reflexivity.
    - intro H; simpl; reflexivity.
    - intro H; simpl; reflexivity.
    - intro H; simpl; reflexivity.
    - intro H; simpl; reflexivity.
  Qed.
  </code></pre>
  
  <p>Is there anyway in Coq to repeat the <code>- intro H; simpl; reflexivity.</code> case proof for non-January months (so I would only have two - or something similar so I do not have to repeat myself)?  Or am I just completely going about this proof the wrong way?</p>