proposition: Lemma rep_interval : forall (k:nat) alpha r1 r2, rep alpha r1 -> rep alpha r2 -> (-(2)/(k+1) <= r1-r2 <= 2/(k+1))%R.
proof: Proof. intros k alpha r1 r2 Hr1 Hr2. assert (H_k_nonneg: 0 <= k); [ apply Z_to_Qle; apply inj_le; auto with arith|]; assert (H_k_one_pos: Zero < k + 1); [natq_zero; qnat_one; natq_S k; natq_S (S k); auto|]. generalize (rep_lb k _ _ Hr1); generalize (rep_lb k _ _ Hr2); generalize (rep_ub k _ _ Hr1); generalize (rep_ub k _ _ Hr2); intros H_r2_u H_r1_u H_r2_l H_r1_l; generalize (Q_to_Rle _ _ (thesis_5_7_9 k alpha)); rewrite Q_to_Rdiv; auto; rewrite Q_to_Rminus; rewrite Q_to_Rplus; rewrite Z_to_Q_to_R_IZR; simpl; fold Qone; rewrite Q_to_R_Qone; intro H_ub_lb; rewrite Rdiv_Ropp_numerator. apply rep_interval_auxiliary with (lb alpha k) (ub alpha k); trivial. change R0 with 0%R; rewrite <- Q_to_R_Qone; rewrite <- Q_to_R_Zero; rewrite <- Q_to_Rplus; apply Rlt_not_eq'; apply Q_to_Rlt; auto. Qed.
imports: digits ub rep Rseries Rdefinitions RIneq Rcomplete QArithSternBrocot(R_addenda) Fourier_solvable_ineqs