proposition: Lemma liminf_incr : forall f:natO-m>U, liminf f == lub f.
proof: Proof. unfold liminf;intros. apply lub_eq_compat; apply fmon_eq_intro; simpl; intro. unfold finf. rewrite (glb_mon (mseq_lift_left f n)); simpl. replace (n+0)%nat with n; auto with arith. Qed.
imports: ALEA(Utheory)