proposition: Lemma x_modulo_PI : forall x, { k : Z | 0 < IZR k * PI - x <= PI }.
proof: Proof. apply x_modulo_B ; apply PI_RGT_0. 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