proposition: Lemma le_liminf_sup : forall f, liminf f <= limsup f.
proof: Proof. unfold liminf,limsup; simpl; intro. rewrite <- Uglb_glb. apply Ole_trans with (Ulub (Finf f)); auto. unfold Finf,Fsup,finf,fsup. apply Ole_trans with (Uglb (fun m : nat => Ulub (fun n : nat => f (n+m)%nat))). apply Ulub_Uglb_exch_le with (f:=fun n m => f (n+m)%nat). apply Uglb_le_compat; simpl; intro. apply Ulub_le_compat; simpl; intro. replace ((x0+x)%nat) with ((x+x0)%nat); auto with arith. Qed.
imports: ALEA(Utheory)