proposition: Lemma xa_in_interval : I xa.
proof: Proof. split. unfold xa in |- *. apply leEq_seq_so_leEq_Lim. simpl in |- *. intro; elim (a_seq_I i); auto. unfold xa in |- *. apply seq_leEq_so_Lim_leEq. simpl in |- *. intro; elim (a_seq_I i); auto. Qed.
imports: CoRN.ftc.Continuity