plus n n injective

Theorem plus_n_n_injective : forall n m,
     n + n = m + m ->
     n = m.
Proof.
  intros n. induction n as [| n'].
  Case "zero". intros m H.
    destruct m.
    SCase "zero". reflexivity.
    SCase "nonzero". inversion H.
  Case "nonzero".
    intros m' H.
    rewrite <- plus_n_Sm in H.
    simpl in H.
    destruct m' as [| m''].
    SCase "m' zero". simpl in H. inversion H.
    SCase "m' nonzero".
       rewrite <- plus_n_Sm in H.
       simpl in H.
       inversion H.
       apply IHn' in H1.
       rewrite -> H1.
       reflexivity.
Qed.