Click on a command or tactic to see a detailed view of its use.

%% %% This is a simple example where induction is needed at a nested rather %% than immediate recursive call. Kind nat type. Type z nat. Type s nat -> nat. Define nat : nat -> prop by nat z ; nat (s N) := nat N. Define even : nat -> prop by even z ; even (s (s N)) := even N. Define odd : nat -> prop by odd (s z) ; odd (s (s N)) := odd N. Theorem even_or_odd : forall N, nat N -> even N \/ odd N. %% An example of mutual induction Define even' : nat -> prop, odd' : nat -> prop by even' z ; odd' (s N) := even' N ; even' (s N) := odd' N. Theorem even'_nat : forall N, even' N -> nat N. Theorem odd'_nat : forall N, odd' N -> nat N.