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