proposition: Lemma x_modulo_B : forall B (B_pos : 0 < B) x, { k : Z | 0 < IZR k * B - x <= B }.
proof: Proof. intros B B_pos x ; pose (k := up (x / B)) ; exists k. destruct (archimed (x / B)) as [x_lb x_ub] ; fold k in x_lb, x_ub. split. apply Rlt_Rminus, Rmult_Rinv_lt_compat_l_rev, x_lb ; assumption. apply Rminus_le_compat_l, Rminus_le_compat_l_rev. apply Rmult_le_reg_r with (/ B). apply Rinv_0_lt_compat ; assumption. transitivity (IZR k - x / B). right ; field ; apply Rgt_not_eq ; assumption. rewrite Rinv_r ; [assumption | apply Rgt_not_eq, B_pos]. Qed.
imports: Rbase Rtactic Lra Ranalysis Rfunctions Rtrigo_facts Rseries_def SeqProp Rextensionality Rpser_usual RIVT Rseries_facts Rsequence_cv_facts MyRIneq Tactics Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis5