proposition: Theorem rep_implies_real_value: forall alpha r, rep alpha r -> real_value alpha = r.
proof: Proof. intros alpha r H_rep. apply SeqProp.cond_eq. intros eps H_eps. set (N:=Zabs_nat (up (2 / eps))). destruct (rep_interval N _ _ _ (rep_real_value alpha) H_rep) as [H1 H2]. elim (Raxioms.archimed (2/eps)); intros H_N _. rewrite <- (Z_of_nat_Zabs_nat_pos (up(2/eps))) in H_N; [|apply Zlt_le_weak; auto]. apply Rbasic_fun.Rabs_def1. apply Rle_lt_trans with (2/((Rdefinitions.IZR N)+1))%R. stepr (2 / (N + 1))%R; auto. rewrite Z_to_Q_to_R_IZR; trivial. apply N_2_epsilon_plus_one; auto. apply Rlt_le_trans with (-(2/((Rdefinitions.IZR N)+1)))%R. apply Ropp_lt_contravar; apply N_2_epsilon_plus_one; auto. stepl (-2 / (N + 1))%R; auto. rewrite Z_to_Q_to_R_IZR; unfold Rdiv; rewrite IZR_Zneg_Zpos; rewrite Ropp_mult_distr_l_reverse; trivial. Qed.
imports: digits ub rep Rseries Rdefinitions RIneq Rcomplete QArithSternBrocot(R_addenda) Fourier_solvable_ineqs