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