Require Export Even.
Require Export Div2.
Require Export Wf_nat.
Require Export ZArith.
Require Export lemmas.
Section power_induction.
Variable P:nat->Prop.
Variable h0:forall n:nat, n=0 -> (P n).
Variable h1:forall n:nat, 0<n -> (even n) -> (P (div2 n)) -> (P n).
Variable h2:forall n:nat, 0<n -> (odd n) -> (P (n-1)) -> (P n).
Definition F :
forall n : nat, forall g : (forall m : nat, m < n -> (P m)), (P n).
intros n g.
case (zerop n).
intros h; apply h0; apply h.
intros h'.
case (even_odd_dec n).
intros Heven.
apply h1.
apply h'.
apply Heven.
apply g.
apply lt_div2.
apply h'.
intros Hodd.
apply h2.
apply h'.
apply Hodd.
apply g.
apply lt_minus_1.
apply h'.
Defined.
Definition power_ind :=
(well_founded_induction_type lt_wf P F).
End power_induction.
power_ind
: forall P : nat -> Prop,
(forall n : nat, n = 0 -> P n) ->
(forall n : nat, 0 < n -> even n -> P (div2 n) -> P n) ->
(forall n : nat, 0 < n -> odd n -> P (n - 1) -> P n) ->
forall a : nat, P a
|