proposition: Lemma f_n_not_in_int : forall (n : nat), (f n) [<] (seq1_lft n) or (seq1_rht n) [<] (f n).
proof: Proof. intros. unfold seq1_lft. unfold seq1_rht. induction n. simpl. left. apply less_plusOne. cut (f (S n)[<]interv_lft (seq_fun (seq1 n) (S n)) or interv_rht (seq_fun (seq1 n) (S n))[<]f (S n)); auto. unfold seq_fun. elim less_cotransitive_unfolded. intros. simpl in |- *. right. auto. intros. simpl in |- *. left. auto. Qed.
imports: CoRN.reals.CReals1