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