proposition: Lemma sin_period_Z x z : sin (x + 2 * PI * IZR z) = sin x.
proof: Proof. pose proof PI_RGT_0. apply trig_period_lemma; try lra. intros. rewrite <- (sin_period x0 k). f_equal. lra. Qed.
imports: Coq(Reals.Ratan Lia Lra Logic.IndefiniteDescription Program.Subset) ZornsLemma(Quotients) Topology(ProductTopology AdjunctionSpace SubspaceTopology RTopology RFuncContinuity Homeomorphisms)