proposition: Lemma lim_bigger: forall (n : nat), (seq1_lft n) [<=] f_lim.
proof: Proof. intros. unfold f_lim. apply str_leEq_seq_so_leEq_Lim. exists n. intros. simpl. unfold seq1_lft. unfold seq1_rht. apply grow_lft; auto. Qed.
imports: CoRN.reals.CReals1