proposition: Theorem rep_real_value : forall alpha, rep alpha (real_value alpha).
proof: Proof. cofix. intros [[ | | ] alpha]. rewrite real_value_L; apply rep_L with alpha; [ apply real_value_base_interval | apply rep_real_value | unfold bisim; apply EqSt_reflex]. rewrite real_value_R; apply rep_R with alpha; [ apply real_value_base_interval | apply rep_real_value | unfold bisim; apply EqSt_reflex]. rewrite real_value_M; apply rep_M with alpha; [ apply real_value_base_interval | apply rep_real_value | unfold bisim; apply EqSt_reflex]. Qed.
imports: digits ub rep Rseries Rdefinitions RIneq Rcomplete QArithSternBrocot(R_addenda) Fourier_solvable_ineqs