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.