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