proposition: Lemma limsup_eq_plus_cte_right : forall k (f : nat -> U), limsup (fun n => (f n) + k) == limsup f + k.
proof: Proof. unfold limsup; intros. apply Oeq_trans with (glb (Imon (UPlus <_> k) @ (Fsup f))); auto. apply glb_eq_compat; apply fmon_eq_intro; simpl; unfold fsup; intros; auto. Qed.
imports: ALEA(Utheory)