proposition: Lemma Bounded_M_auxiliary_3: forall (c d:Q), Zero<=d+c -> Zero <= d-c -> Zero <= d.
proof: Proof. intros c d H1 H2; apply Qmult_resp_Qle_pos_r 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