proposition: Lemma fsup_mon : forall (f:nat->U) n, fsup f (S n) <= fsup f n.
proof: Proof. unfold fsup; intros. apply Ulub_le; intros. replace (S n+n0)%nat with (n+S n0)%nat; try lia. apply le_Ulub with (f:=fun k : nat => f (n+k)%nat). Qed.
imports: ALEA(Utheory)