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