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