proposition: Lemma Is_refining_T_h_minusplus_efg_sign_dec: forall a b c d e f g h, Is_refining_T (((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 <= a - b + c - d - e + f - g + h /\ Zero<e+f+g+h /\ Zero<e-f-g+h /\ Zero< -e-f+g+h /\ Zero< -e+f-g+h /\ Zero<h \/ 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 /\ e+f+g+h<Zero /\ e-f-g+h<Zero /\ -e-f+g+h<Zero /\ -e+f-g+h<Zero /\ h<Zero.
proof: Proof. intros a b c d e f g h [[[H1 [H2 [H3 H4]]]|[H1 [H2 [H3 H4]]]] [[H5[H6[H7[H8[H9[H10[H11 H12]]]]]]]|[H5[H6[H7[H8[H9[H10[H11 H12]]]]]]]]]; unfold fst, snd in H1, H2, H3, H4, H5, H6, H7, H8, H9, H10, H11, H12. generalize (Bounded_T_auxiliary_1 _ _ _ _ H1 H2 H3 H4); intros Hh; tauto. decompose record (Is_refining_T_auxiliary_2 _ _ _ _ _ _ _ _ H5 H6 H7 H8 H9 H10 H11 H12); contradiction. decompose record (Is_refining_T_auxiliary_1 _ _ _ _ _ _ _ _ H5 H6 H7 H8 H9 H10 H11 H12); contradiction. generalize (Bounded_T_auxiliary_2 _ _ _ _ H1 H2 H3 H4); intros Hh; tauto. Qed.
imports: digits Refining_M Bounded_T QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier