proposition: Lemma liminf_inv : forall f : nat -> U, liminf (fun x => [1-]f x) == [1-] limsup f.
proof: Proof. unfold limsup, liminf; intros. unfold glb. rewrite Uinv_inv. apply lub_eq_compat; apply fmon_eq_intro; intro n; simpl; unfold finf,fsup,Uglb; Usimpl. apply Ulub_eq_compat; apply ford_eq_intro; intro m; auto. Qed.
imports: ALEA(Utheory)