proposition: Lemma intervals_smaller : forall N : nat, seq1_rht N[-]seq1_lft N [<=]Small[^]N.
proof: Proof. intros. induction N. astepl (([1][-][0]):IR). astepr ([1]:IR). astepl ([1]:IR). apply leEq_reflexive. unfold seq1_lft. unfold seq1_rht. simpl. astepr ((Two [-] [1]):IR); rational. apply leEq_transitive with (Small[*](seq1_rht N[-]seq1_lft N)); auto. apply next_smaller; auto. astepr (Small[*]Small[^]N). apply mult_resp_leEq_lft; auto. apply small_greater_zero. Qed.
imports: CoRN.reals.CReals1