proposition: Lemma liminf_decr : forall f:natO-m>UI, liminf f == glb f.
proof: Proof. unfold liminf; intros. apply Oeq_trans with (lub (fmon_cte natO (glb f))); auto. apply lub_eq_compat; apply fmon_eq_intro; simpl; unfold finf; intros. apply Oeq_trans with (glb (mseq_lift_left f n)). apply Oeq_trans with (Uglb (mseq_lift_left f n)); auto. apply Oeq_sym; auto. Qed.
imports: ALEA(Utheory)