proposition: Lemma Bounded_T_M_r:forall a b c d e f g h, Bounded_T (a, b, (c, d), (e, f, (g, h))) -> forall y, - Qone <= y/\ y <= Qone -> Bounded_M (a*y + b, c*y + d, (e*y + f, g*y + h)).
proof: Proof. intros a b c d e f g h H_bound y [Hyl Hyu]. assert (Hy_lr:(-1<= y <= 1 )%R); [realify_Q; intros; split; trivial|]. remember H_bound as H; clear HeqH; destruct H as [[H1 [H2 [H3 H4]]]|[H1 [H2 [H3 H4]]]]; unfold fst, snd in H1,H2,H3,H4. left; unfold fst, snd; assert (Hh:=Bounded_T_auxiliary_1 _ _ _ _ H1 H2 H3 H4); split. assert (Hdenom:= Bounded_T_pos _ _ _ _ _ _ _ _ 1%R y H_bound Hh one_is_in_base_interval Hy_lr); apply Q_to_R_Qlt; realify_Q_goal; ring_exact_R Hdenom. assert (Hdenom:= Bounded_T_pos _ _ _ _ _ _ _ _ (-1)%R y H_bound Hh min_one_is_in_base_interval Hy_lr); apply Q_to_R_Qlt; realify_Q_goal; ring_exact_R Hdenom. right; unfold fst, snd; assert (Hh:=Bounded_T_auxiliary_2 _ _ _ _ H1 H2 H3 H4); split. assert (Hdenom:= Bounded_T_neg _ _ _ _ _ _ _ _ 1%R y H_bound Hh one_is_in_base_interval Hy_lr); apply Q_to_R_Qlt; realify_Q_goal; ring_exact_R Hdenom. assert (Hdenom:= Bounded_T_neg _ _ _ _ _ _ _ _ (-1)%R y H_bound Hh min_one_is_in_base_interval Hy_lr); apply Q_to_R_Qlt; realify_Q_goal; ring_exact_R Hdenom. Qed.
imports: digits Bounded_M Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs