proposition: Lemma Bounded_T_auxiliary_5:forall e f g h x y, Zero <= e + f + g + h -> Zero <= e - f - g + h -> Zero <= - e - f + g + h -> Zero <= - e + f - g + h -> (-1<=x<=1)%R->(-1<=y<=1)%R->(0<=e*x*y+f*x+g*y+h)%R.
proof: Proof. intros e f g h x y H1 H2 H3 H4 Hx Hy. assert (H_hf1:Zero<=h-f); [apply Qmult_resp_Qle_pos_r with (Qone+Qone); auto; stepl Zero; auto; stepr ((e-f-g+h)+(-e-f+g+h)); auto; ring|]. assert (H_hf2:Zero<=h+f); [apply Qmult_resp_Qle_pos_r with (Qone+Qone); auto; stepl Zero; auto; stepr ((e+f+g+h)+(-e+f-g+h)); auto; ring|]. assert (H_hg1:Zero<=h-g); [apply Qmult_resp_Qle_pos_r with (Qone+Qone); auto; stepl Zero; auto; stepr ((e-f-g+h)+(-e+f-g+h)); auto; ring|]. assert (H_hg2:Zero<=h+g); [apply Qmult_resp_Qle_pos_r with (Qone+Qone); auto; stepl Zero; auto; stepr ((e+f+g+h)+(-e-f+g+h)); auto; ring|]. stepr ((e*y+f)*x+ (g*y+h))%R; [|ring]. destruct (Rtrichotomy_inf 0 (e*y+f)) as [[Hef|Hef]|Hef]. apply Bounded_M_pos_auxiliary_3; trivial; stepr (Qminus g e * y + Qminus h f)%R; [|realify_Q_goal; ring]; apply Bounded_M_auxiliary_5; trivial; [ring_exact_Q H3|ring_exact_Q H2]. rewrite <- Hef; stepr (g*y+h)%R; [|ring]; apply Bounded_M_auxiliary_5; assumption. apply Bounded_M_pos_auxiliary_4; trivial; stepr (Qplus g e * y + Qplus h f)%R; [|realify_Q_goal; ring]. apply Bounded_M_auxiliary_5; trivial; [ring_exact_Q H1|ring_exact_Q H4]. Qed.
imports: digits Refining_M Bounded_T QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier