proposition: Lemma sin_2PI_neg : forall x, sin (2 * PI - x) = - sin x.
proof: Proof. intro. unfold Rminus. now rewrite sin_2PI, sin_neg. Qed.
imports: Coq(Reals.Ratan Lia Lra Logic.IndefiniteDescription Program.Subset) ZornsLemma(Quotients) Topology(ProductTopology AdjunctionSpace SubspaceTopology RTopology RFuncContinuity Homeomorphisms)