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