proposition: Lemma rep_drop_in_range:forall alpha r n, rep alpha r -> (-1<=as_Moebius (product_init_rev alpha n) r<=1)%R.
proof: Proof. intros alpha r n H_rep; apply rep_inv_interval with (drop n alpha); apply rep_drop; trivial. Qed.
imports: digits Refining_M Streams_addenda Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs