proposition: Lemma x_modulo_2PI : forall x, { k | 0 < IZR (k) * (2 * PI) + x <= 2 * PI }.
proof: Proof. intros x ; pose (k := - x / (2 * PI)) ; exists (up k) ; destruct (archimed k) as [k_lb k_ub]. split. rewrite Rplus_comm ; apply Rminus_lt_compat_l_rev, Rmult_Rinv_lt_compat_l_rev. apply Rmult_lt_0_compat ; [lra | apply PI_RGT_0]. rewrite Rminus_0_l ; apply k_lb. transitivity ((IZR (up k) - k) * (2 * PI)). right ; unfold k ; field ; apply Rgt_not_eq, PI_RGT_0. transitivity (1 * (2 * PI)) ; [| right ; ring] ; apply Rmult_le_compat_r. left ; apply Rmult_lt_0_compat ; [lra | apply PI_RGT_0]. assumption. Qed.
imports: Rbase AltSeries Rseries_def Rtrigo_facts Ratan Cpow_plus Complex Lra MyRIneq