# A weird induction principle

Consider the following context :
Section weird_induc_proof.
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
theorem itself.

This exercise was suggested by H. Sudbrock.
## Solution

Look at the file weird_induc.v.

Going home

Pierre Castéran