fact: Definition f_inv : ClosedUnitInterval -> S1 := induced_function (fun x => exist _ (circle_cover (subspace_inc _ x)) _) (SpaceAdjunction_equivalence _) f_inv_helper.
imports: Coq(Reals.Ratan Lia Lra Logic.IndefiniteDescription Program.Subset) ZornsLemma(Quotients) Topology(ProductTopology AdjunctionSpace SubspaceTopology RTopology RFuncContinuity Homeomorphisms)