proposition: Lemma IIim_incl_stable : forall (I J:natO-m>IUord), (forall n, Iincl (I n) (J n)) -> Iincl (Ilim I) (Ilim J).
proof: Proof. intros; apply Iincl_lim. intros; apply Iincl_trans with (I n); auto. Qed.
imports: ALEA(Utheory)