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