proposition: Lemma U_conversion_rate2 : forall m n : nat, 4 <= m -> m <= n -> AbsSmall (dstart_r[-]dstart_l[/] nring (S m)[//]nringS_ap_zero _ m) (U m[-]U n).
proof: Proof. intros. apply AbsSmall_leEq_trans with (e1 := Length _ (dIntrvl m)). apply less_leEq. astepl ((Two [/]ThreeNZ)[^]m[*](dstart_r[-]dstart_l)). rstepr (([1][/] nring (S m)[//]nringS_ap_zero _ m)[*](dstart_r[-]dstart_l)). apply mult_resp_less. apply a_familiar_simple_inequality. assumption. apply shift_zero_less_minus. apply dl_less_dr. apply eq_symmetric_unfolded. apply Length_dIntrvl. unfold Length in |- *. apply AbsSmall_subinterval; apply less_leEq. change (V m[<]U m) in |- *. apply U_m_n_V. constructor. change (V m[<]U n) in |- *. apply U_m_n_V. assumption. change (U m[<]W m) in |- *. apply U_m_n_W. constructor. change (U n[<]W m) in |- *. apply U_m_n_W. assumption. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon