Variable P : nat -> Prop.
Variable f : nat -> nat.

Hypothesis f_strict_mono:  forall (n p : nat), lt n p -> lt (f n) (f p). 
Hypothesis f_o: lt 0 (f 0).

Hypothesis PO: P O.
Hypothesis P_Sn_n: forall (n:nat), P (S n) -> P n.
Hypothesis f_P: forall (n:nat), P n -> P (f n).

Print lt.

Theorem weird_induc: forall (n:nat), P n.