Example of case statement with Coq from Coq Art

ex6_10.v

(* exercise 6.10 from Coq Art *)

 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.

Definition is_January : month -> Prop :=
  month_rect (fun m : month => Prop)
    True
    False False False False False False False False False False False.

Eval compute in (is_January January).
Eval compute in (is_January December).

Definition is_January' (m : month) : Prop :=
  match m with
  | January => True
  | other   => False
  end.

Eval compute in (is_January' January).
Eval compute in (is_January' December).

Theorem is_Januarys_eq :
  forall m : month, is_January = is_January'.
Proof.
  intro m.
  compute; reflexivity.
Qed.

Theorem is_January_eq_January :
  forall m : month, m = January -> is_January m = True.
Proof.
  intros m H.
  rewrite H.
  compute; reflexivity.
Qed.

(* from this answer http://stackoverflow.com/a/43826990/2370606 *)
Theorem is_January_neq_not_January :
  forall m : month, m <> January -> is_January m = False.
Proof.
  induction m; try reflexivity.
  contradiction.
Qed.

Theorem is_January_neq_not_January' :
  forall m : month, m <> January -> is_January m = False.
Proof.
  induction m; try (split; unfold not; intro H'; inversion H'; fail).
  contradiction.
Qed.

Theorem is_January_neq_not_January'' :
  forall m : month, m <> January -> is_January m = False.
Proof.
  induction m; try reflexivity || contradiction.
Qed.

Theorem is_January_neq_not_January''' :
  forall m : month, m <> January -> is_January m = False.
Proof.
  destruct m; easy.
Qed.

Be thank you to Nobody on StackOverflow for helping me with a more elegant proof. http://stackoverflow.com/a/43826990/2370606