proposition: Lemma unbnd_f : forall m, {n : nat | m < f n}.
proof: Proof. simple induction m. elim (crescF 0). intros n Hn. exists n. inversion_clear Hn. apply Nat.le_lt_trans with (f 0); auto with arith. intros n H. elim H; clear H; intros n' Hn'. elim (crescF n'). intros i Hi; elim Hi; clear Hi; intros Hi Hi'. exists i. apply Nat.le_lt_trans with (f n'); auto. Qed.
imports: CoRN.reals.Max_AbsIR CoRN.algebra.Expon CoRN.algebra.CPoly_ApZero