proposition: Lemma AbsSmall_U_V : forall n : nat, AbsSmall ((Two [/]ThreeNZ)[^]n[*](dstart_r[-]dstart_l)) (U n[-]V n).
proof: Proof. intros. split; apply less_leEq. apply less_wdr with (y := Length R1 (dIntrvl n) [/]TwoNZ). apply less_wdl with (x := [--](Length R1 (dIntrvl n))). apply plus_cancel_less with (z := Length R1 (dIntrvl n)). rstepl ([0]:R1). apply plus_resp_pos. apply pos_div_two. unfold Length in |- *. apply shift_zero_less_minus. apply is_interval. unfold Length in |- *. apply shift_zero_less_minus. apply is_interval. apply un_op_wd_unfolded. apply Length_dIntrvl. apply eq_symmetric_unfolded. apply U_minus_V. apply U_V_upper. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon