proposition: Lemma Bounded_T_auxiliary_3: forall (e f g h:Q), Zero<=e+f+g+h -> Zero<=e-f-g+h -> Zero<= -e-f+g+h -> Zero<= -e+f-g+h -> Zero<=h.
proof: Proof. intros e f g h H1 H2 H3 H4; apply Qmult_resp_Qle_pos_r with (Qone+Qone+Qone+Qone); auto; stepl Zero; auto; stepr ((e+f+g+h)+(e-f-g+h)+(-e-f+g+h)+(-e+f-g+h)); auto; ring. Qed.
imports: digits Bounded_M Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs