proposition: Lemma Is_refining_M_d_minusplus_c_sign_dec: forall a b c d, Is_refining_M ((a,b),(c,d))-> (Qle Zero (Qplus (Qplus (Qplus a b) c) d) /\ Qle Zero (Qplus (Qminus (Qminus a b) c) d) /\ Qle Zero (Qplus (Qplus (Qminus (Qopp a) b) c) d) /\ Qle Zero (Qplus (Qminus (Qplus (Qopp a) b) c) d) /\ Qlt Zero (Qminus d c)/\Qlt Zero (Qplus d c)/\Qlt Zero d) \/ (Qle (Qplus (Qplus (Qplus a b) c) d) Zero /\ Qle (Qplus (Qminus (Qminus a b) c) d) Zero /\ Qle (Qplus (Qplus (Qminus (Qopp a) b) c) d) Zero /\ Qle (Qplus (Qminus (Qplus (Qopp a) b) c) d) Zero /\ Qlt (Qminus d c) Zero/\Qlt (Qplus d c) Zero/\Qlt d Zero).
proof: Proof. intros a b c d [[[H0 H0']|[H0 H0']] [[H1 [H2 [H3 H4]]]|[H1 [H2 [H3 H4]]]]]; unfold fst, snd in H0, H0', H1, H2, H3, H4; first [generalize (Bounded_M_auxiliary_1 _ _ H0 H0')|generalize (Bounded_M_auxiliary_2 _ _ H0 H0')] ;intros Hd; tauto || first [decompose record (Is_refining_M_auxiliary_1 _ _ _ _ H1 H2 H3 H4) |decompose record (Is_refining_M_auxiliary_2 _ _ _ _ H1 H2 H3 H4)]; contradiction. Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M