proposition: Lemma neg_cos_PI (x : R): cos (x - PI) = - cos x.
proof: Proof. rewrite <- (cos_period _ 1). simpl. replace (x - PI + 2 * 1 * PI) with (x + PI) by lra. apply neg_cos. Qed.
imports: Coq(Reals.Ratan Lia Lra Logic.IndefiniteDescription Program.Subset) ZornsLemma(Quotients) Topology(ProductTopology AdjunctionSpace SubspaceTopology RTopology RFuncContinuity Homeomorphisms)