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