proposition: Lemma Is_refining_T_auxiliary_1: forall (a b c d e f g h:Q), Zero <= a + b + c + d + e + f + g + h -> Zero <= - a - b - c - d + e + f + g + h -> Zero <= a - b - c + d + e - f - g + h -> Zero <= - a + b + c - d + e - f - g + h -> Zero <= - a - b + c + d - e - f + g + h -> Zero <= a + b - c - d - e - f + g + h -> Zero <= - a + b - c + d - e + f - g + h -> Zero <= a - b + c - d - e + f - g + h -> Zero<=h/\ Zero<=e+f+g+h /\ Zero<=e-f-g+h /\ Zero<=-e-f+g+h /\ Zero<=-e+f-g+h.
proof: Proof. let t_local:= apply Qmult_resp_Qle_pos_r with (Qone+Qone); auto; stepl Zero; auto in ( intros a b c d e f g h H1 H2 H3 H4 H5 H6 H7 H8; repeat split; [ apply Qmult_resp_Qle_pos_r with (Qone+Qone+Qone+Qone+Qone+Qone+Qone+Qone); auto; stepl Zero; auto; stepr ((a + b + c + d + e + f + g + h)+( - a - b - c - d + e + f + g + h)+(a - b - c + d + e - f - g + h)+ (- a + b + c - d + e - f - g + h)+(- a - b + c + d - e - f + g + h)+(a + b - c - d - e - f + g + h)+ (- a + b - c + d - e + f - g + h)+(a - b + c - d - e + f - g + h)); repeat first [apply Qle_plus_pos_pos; trivial]; ring | t_local | t_local | t_local | t_local ]; idtac). stepr ((a + b + c + d + e + f + g + h)+(- a - b - c - d + e + f + g + h)); auto; ring. stepr ((a - b - c + d + e - f - g + h)+(- a + b + c - d + e - f - g + h)); auto; ring. stepr ((a + b - c - d - e - f + g + h)+(- a - b + c + d - e - f + g + h)); auto; ring. stepr ((-a + b - c + d - e + f - g + h)+(a - b + c - d - e + f - g + h)); auto; ring. Qed.
imports: digits Refining_M Bounded_T QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier