proposition: Lemma lim_Iincl : forall (I:natO-m>IUord) n, Iincl (Ilim I) (I n).
proof: Proof. unfold Ilim,Iincl; simpl; split. apply le_lub with (f:=Low @ I) (n:=n). apply glb_le with (f:=Up @ I) (n:=n). Qed.
imports: ALEA(Utheory)