A weird induction principle
Consider the following context :
Variable P : nat -> Prop.
Variable f : nat -> nat.
Hypothesis f_strict_mono : forall n p:nat, n < p -> f n < f p.
Hypothesis f_O : 0 < f 0.
Hypothesis P0 : P 0.
Hypothesis P_Sn_n : forall n:nat, P (S n) -> P n.
Hypothesis f_P : forall n:nat, P n -> P (f n).
Prove the following theorem :
Theorem weird_induc : forall n:nat, P n.
Hints and Notes
It would be a good idea to show some lemmas before proving yhe
This exercise was suggested by H. Sudbrock.
Look at the file weird_induc.v.