proposition: Lemma Bounded_T_M_4:forall a b c d e f g h,Bounded_T (((a,b),(c,d)),((e,f),(g,h))) -> Bounded_M (- a + b, - c + d, (- e + f, - g + h)).
proof: Proof. intros a b c d e f g h [[H1 [H2 [H3 H4]]]|[H1 [H2 [H3 H4]]]]; unfold fst, snd in H1,H2, H3, H4; [left|right]; unfold fst, snd; split; [ ring_exact_Q H4 | ring_exact_Q H2 | ring_exact_Q H4 | ring_exact_Q H2 ]. Qed.
imports: digits Bounded_M Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs