proposition: Lemma Is_refining_M_auxiliary_1: forall (a b c d:Q), Zero <= a + b + c + d -> Zero <= a - b - c + d -> Zero <= - a - b + c + d -> Zero <= - a + b - c + d -> Zero<=d/\Zero<=d-c/\Zero<=d+c/\Zero<=d-b/\Zero<=d+b/\Zero<=d-a/\Zero<=d+a.
proof: Proof. let t_local:= apply Qmult_resp_Qle_pos_r with (Qone+Qone); auto; stepl Zero; auto in ( intros a b c d H1 H2 H3 H4; repeat split; [ apply Qmult_resp_Qle_pos_r with (Qone+Qone+Qone+Qone); auto; stepl Zero; auto; stepr ((a + b + c + d)+(- a - b + c + d)+(a - b - c + d)+(- a + b - c + d)) | t_local; stepr ((a - b - c + d)+(- a + b - c + d)) | t_local; stepr ((a + b + c + d)+(- a - b + c + d)) | t_local; stepr ((a - b - c + d)+(- a - b + c + d)) | t_local; stepr ((a + b + c + d)+(- a + b - c + d)) | t_local; stepr ((- a - b + c + d)+(- a + b - c + d)) | t_local; stepr ((a + b + c + d)+(a - b - c + d)) ]; auto; ring). Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M