proposition: Lemma next_smaller : forall (I : interv) (n : nat), seq1_rht (S n)[-]seq1_lft (S n) [<=] Small [*](seq1_rht n[-]seq1_lft n).
proof: Proof. intros. unfold seq1_lft. unfold seq1_rht. astepl (interv_rht (seq_fun (seq1 n) (S n))[-]interv_lft (seq_fun (seq1 n) (S n))). unfold seq_fun. case (less_cotransitive_unfolded IR _ _ (less_pres_lft_rht _ _ (interv_lft_rht (seq1 n))) (f (S n))). intros. simpl. apply leEq_transitive with (rht (interv_lft (seq1 n)) (interv_rht (seq1 n))[-]interv_lft (seq1 n)). apply minus_resp_leEq. apply less_leEq. apply less_pres_lft_rht. apply interv_lft_rht. apply eq_imp_leEq. apply smaller_rht. intros. simpl. apply leEq_transitive with (interv_rht (seq1 n)[-]lft (interv_lft (seq1 n)) (interv_rht (seq1 n))). apply minus_resp_leEq_rht. apply less_leEq. apply less_pres_lft_rht. apply interv_lft_rht. apply eq_imp_leEq. apply smaller_lft. Qed.
imports: CoRN.reals.CReals1