proposition: Lemma G_conversion_rate_resp_x : forall (x : R1) (m : nat), 4 <= m -> AbsSmall (inj_Q R1 (start_r x[-]start_l x[/] nring (S m)[//]nringS_ap_zero _ m)) (inj_Q R1 (G x m)[-]x).
proof: Proof. intros. apply AbsSmall_leEq_trans with (e1 := inj_Q R1 (Length _ (Intrvl x m))). apply less_leEq. apply inj_Q_less. 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 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 |- *. astepl (inj_Q R1 (sndT (Intrvl x m))[-]inj_Q R1 (fstT (Intrvl x m))). apply AbsSmall_subinterval; apply less_leEq. apply inj_Q_less. apply G_m_n_lower. constructor. apply x_in_Intrvl_l. apply inj_Q_less. apply G_m_n_upper. constructor. apply x_in_Intrvl_r. Qed.
imports: CoRN.reals.Q_in_CReals