proposition: Lemma Bounded_T_auxiliary_1: 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 Qlt_Qmult_cancel_l 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