proposition: Lemma Bounded_M_denom_nonvanishing_M:forall mu, Bounded_M mu -> (forall r, (-1 <= r <= 1)%R -> denom_nonvanishing_M mu r).
proof: Proof. intros ((a,b),(c,d)) H_bounded r Hr; red; simpl; apply Bounded_M_nonzero_denum with a b; assumption. Qed.
imports: digits Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs