ボクには ; 使ったのは気持ちはなんとなくわかるけど imihu だったので一つずつ証明した。

daigakusei.v

Inductive even : nat -> Prop :=
| even_O : even 0
| even_S : forall n, odd n -> even (S n)
with odd : nat -> Prop :=
| odd_S : forall n, even n -> odd (S n).

Scheme even_mut := Induction for even Sort Prop
  with odd_mut := Induction for odd Sort Prop.

Theorem daigakuseinosuugakuryoku : forall n m,
  even n -> odd m -> odd (m + n).
Proof.
intros n m H H0.
revert m H0.
apply odd_mut with (fun m e => even (m + n)).

simpl.
assumption.

intros.
simpl.
apply even_S.
assumption.

intros.
simpl.
apply odd_S.
assumption.
Qed.

-------------------------------------------------------

別解（こっちのほうがめんどくさいぞ！）

Require Import Arith.
Inductive even : nat -> Prop :=
| even_O : even 0
| even_S : forall n, odd n -> even (S n)
with odd : nat -> Prop :=
| odd_S : forall n, even n -> odd (S n).

Scheme even_mut := Induction for even Sort Prop
  with odd_mut := Induction for odd Sort Prop.

Theorem daigakuseinosuugakuryoku : forall n m,
  even n -> odd m -> odd (m + n).
Proof.
intros n m H H0.
revert n H.
apply even_mut with (fun n e => even (m + n)).

rewrite plus_comm.
simpl.
assumption.

intros.
rewrite <- plus_Snm_nSm.
simpl.
apply odd_S.
assumption.

intros.
rewrite <- plus_Snm_nSm.
simpl.
apply even_S.
assumption.
Qed.