proposition: Lemma rep_inv_interval : forall alpha r, rep alpha r -> (-1 <= r <= 1)%R.
proof: Proof. intros alpha r H_rep; inversion_clear H_rep; [ apply conjL_range_weak| apply conjR_range_weak | apply conjM_range_weak]; trivial. Qed.
imports: digits Refining_M Streams_addenda Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs