proposition: Lemma lim_smaller: forall (n : nat), f_lim [<=] (seq1_rht n).
proof: Proof. intros. unfold f_lim. apply str_seq_leEq_so_Lim_leEq. exists n. intros. simpl. unfold seq1_lft. unfold seq1_rht. apply leEq_transitive with (interv_rht (seq1 i)). apply less_leEq. apply interv_lft_rht. apply grow_rht. auto. Qed.
imports: CoRN.reals.CReals1