proposition: Lemma Is_refining_M_auxiliary_2: forall (a b c d:Q), 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<=Zero.
proof: Proof. let t_local:= apply Qmult_resp_Qle_pos_r with (Qone+Qone); auto; stepr 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; stepr Zero; auto; stepl ((a + b + c + d)+(- a - b + c + d)+(a - b - c + d)+(- a + b - c + d)) | t_local; stepl ((a - b - c + d)+(- a + b - c + d)) | t_local; stepl ((a + b + c + d)+(- a - b + c + d)) | t_local; stepl ((a - b - c + d)+(- a - b + c + d)) | t_local; stepl ((a + b + c + d)+(- a + b - c + d)) | t_local; stepl ((- a - b + c + d)+(- a + b - c + d)) | t_local; stepl ((a + b + c + d)+(a - b - c + d)) ]; auto; ring). Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M