proposition: Lemma i_f_i : forall i:nat, i <= iterate _ f i 1.
proof: Proof. induction i. auto with arith. cut (iterate _ f i 1 < iterate _ f (S i) 1). intros. clear P_Sn_n f_strict_mono f_1 f_P. lia. elim i;simpl;auto. Qed.
imports: Arith Lia