proposition: Lemma finf_fn : forall f n, finf f n <= f n.
proof: Proof. unfold finf; intros. pattern n at 2; replace n with (n+O)%nat; auto with arith. apply Uglb_le with (f:=fun k : nat => f (n+k)%nat) (n:=O). Qed.
imports: ALEA(Utheory)