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