proposition: Lemma G_conversion_rate2 : forall (x : R1) (m n : nat), 4 <= m -> m <= n -> AbsSmall (start_r x[-]start_l x[/] nring (S m)[//]nringS_ap_zero _ m) (G x m[-]G x n).
proof: Proof. intros. apply AbsSmall_leEq_trans with (Length _ (Intrvl x m)). astepl ((Two [/]ThreeNZ)[^]m[*](start_r x[-]start_l x)). rstepr (([1][/] nring (S m)[//]nringS_ap_zero _ m)[*](start_r x[-]start_l x)). apply less_leEq. apply mult_resp_less. apply a_simple_inequality. assumption. apply shift_zero_less_minus. apply l_less_r. apply eq_symmetric_unfolded. apply Length_Intrvl. unfold Length in |- *. apply AbsSmall_subinterval; apply less_leEq. apply G_m_n_lower. constructor. apply G_m_n_lower. assumption. apply G_m_n_upper. constructor. apply G_m_n_upper. assumption. Qed.
imports: CoRN.reals.Q_in_CReals