proposition: Lemma intervals_embed : forall N m : nat, N <= m -> AbsSmall (R:=IR) (seq1_rht N[-]seq1_lft N) (seq1_lft m[-]seq1_lft N).
proof: Proof. intros. unfold seq1_rht. unfold seq1_lft. unfold AbsSmall. split. apply leEq_transitive with ([0]:IR). astepr ([--][0]:IR). apply inv_resp_leEq. apply shift_leEq_lft. apply less_leEq. apply interv_lft_rht. apply shift_leEq_lft. 2: apply minus_resp_leEq. apply grow_lft; auto. apply leEq_transitive with (interv_rht (seq1 m)). apply less_leEq. apply interv_lft_rht. apply grow_rht; auto. Qed.
imports: CoRN.reals.CReals1