proposition: Lemma rep_L_inv_interval : forall alpha r, rep (Cons LL alpha) r -> (-1 <= r <= 0)%R.
proof: Proof. intros alpha r H_rep; inversion_clear H_rep as [alpha0 y x [H1 H2] _ _|alpha0|alpha0]; try (inversion H1; discriminate H2); split; [ apply conjL_range_l | apply conjL_range_r]; trivial. Qed.
imports: digits Refining_M Streams_addenda Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs