blob: 0a0812711c84c0106c77e24a94e7d2bf1f2aa964 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Set Automatic Introduction.
Inductive even : nat -> Prop :=
| even_0 : even 0
| even_odd : forall n, odd n -> even (S n)
with odd : nat -> Prop :=
| odd_1 : odd 1
| odd_even : forall n, even n -> odd (S n).
Lemma foo {n : nat} (E : even n) : even (S (S n))
with bar {n : nat} (O : odd n) : odd (S (S n)).
Proof. destruct E. constructor. constructor. apply even_odd. apply (bar _ H).
destruct O. repeat constructor. apply odd_even. apply (foo _ H).
Defined.
|
