proposition: Lemma Bounded_M_auxiliary_2: forall (c d:Q), d+c<Zero -> d-c<Zero -> d<Zero.
proof: Proof. intros c d H1 H2; apply Qlt_Qmult_cancel_l with (Qone+Qone); auto; stepr Zero; auto; stepl ((d+c)+(d-c)); auto ;ring. Qed.
imports: digits Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs