proposition: Lemma liminf_eq_plus_cte_right : forall k (f : nat -> U), liminf (fun n => (f n) + k) == liminf f + k.
proof: Proof. unfold liminf; intros. apply Oeq_trans with (lub (UPlus <_> k @ (Finf f))); auto. apply lub_eq_compat; apply fmon_eq_intro; simpl; unfold finf; intros; auto. Qed.
imports: ALEA(Utheory)