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)); intros; try constructor; assumption.
Qed.