proposition: Lemma sin_2PI : forall x, sin (2 * PI + x) = sin x.
proof: Proof. intro. replace (2 * PI + x) with (x + PI + PI) by lra. rewrite neg_sin, neg_sin. lra. Qed.
imports: Coq(Reals.Ratan Lia Lra Logic.IndefiniteDescription Program.Subset) ZornsLemma(Quotients) Topology(ProductTopology AdjunctionSpace SubspaceTopology RTopology RFuncContinuity Homeomorphisms)