proposition: Lemma rep_ub: forall (k:nat) alpha r, rep alpha r -> (r<=(ub alpha k))%R.
proof: Proof. induction k. intros alpha r H_rep; unfold ub; rewrite Z_to_Q_to_R_IZR; simpl; elim (rep_inv_interval _ _ H_rep); trivial. intros [[ | | ] alpha] r H_rep; rewrite ub_S_n; unfold hd,tl; set (u':=(ub alpha k)). assert (H_u'_one_nonneg: Zero <= u'+1); [ stepr (u'-(Qopp 1)); try ring; apply Qle_Qminus_Zero; subst u'; apply ub_is_in_base_interval_low|]. assert (H_u'_three_pos: Zero < u'+3); [ apply Qle_lt_trans with (u'+1); auto; apply Qlt_Zero_Qminus; stepr 2; auto; qnat_S 2; qnat_S 1; qnat_one; ring|]. generalize (Q_to_Rle _ _ H_u'_one_nonneg); generalize (Q_to_Rlt _ _ H_u'_three_pos); do 2 rewrite Q_to_Rplus; rewrite Q_to_R_Zero; do 2 rewrite Z_to_Q_to_R_IZR; intros H1 H2; simpl in H1,H2. rewrite as_Moebius_Q_L; trivial; natZ_numerals; rewrite Q_to_Rdiv; auto; rewrite Q_to_Rplus; rewrite Q_to_Rminus; repeat rewrite Z_to_Q_to_R_IZR; simpl; elim (rep_L_inv_interval _ _ H_rep); intros Hr1 Hr2; generalize (IHk _ _ (rep_L_inv _ _ H_rep)); clear IHk; fold u'; intro IHk; apply rep_ub_auxiliary_L; auto; stepr (u'+(2+1))%R; auto; ring. assert (H_min_u'_one_nonneg: Zero <= -u'+1); [stepr (1-u'); try ring; apply Qle_Qminus_Zero; subst u'; apply ub_is_in_base_interval_up|]. assert (H_min_u'_three_pos: Zero < -u'+3); [ apply Qle_lt_trans with ((-u')+1); auto;apply Qlt_Zero_Qminus; stepr 2; auto; qnat_S 2; qnat_S 1; qnat_one; ring|]. generalize (Q_to_Rle _ _ H_min_u'_one_nonneg); generalize (Q_to_Rlt _ _ H_min_u'_three_pos); do 2 rewrite Q_to_Rplus; rewrite Q_to_R_Zero; rewrite Q_to_Ropp; do 2 rewrite Z_to_Q_to_R_IZR; intros H1 H2; simpl in H1,H2. rewrite as_Moebius_Q_R; trivial; natZ_numerals; rewrite Q_to_Rdiv; auto; repeat rewrite Q_to_Rplus; rewrite Q_to_Ropp; repeat rewrite Z_to_Q_to_R_IZR; simpl; elim (rep_R_inv_interval _ _ H_rep); intros Hr1 Hr2; generalize (IHk _ _ (rep_R_inv _ _ H_rep)); clear IHk; fold u'; intro IHk; apply rep_ub_auxiliary_R; auto; stepr (-u'+(2+1))%R; auto; ring. rewrite as_Moebius_Q_M; natZ_numerals; rewrite Q_to_Rdiv; auto; rewrite Z_to_Q_to_R_IZR; simpl; elim (rep_M_inv_interval _ _ H_rep); intros Hr1 Hr2; generalize (IHk _ _ (rep_M_inv _ _ H_rep)); clear IHk; fold u'; intro IHk; apply rep_ub_auxiliary_M; auto. Qed.
imports: digits ub rep Rseries Rdefinitions RIneq Rcomplete QArithSternBrocot(R_addenda) Fourier_solvable_ineqs