fact: Definition f1 (p : R*R) : R := if (Rle_lt_dec (snd p) 0) then 1 - acos (fst p) / (2 * PI) else acos (fst p) / (2 * PI).
imports: Coq(Reals.Ratan Lia Lra Logic.IndefiniteDescription Program.Subset) ZornsLemma(Quotients) Topology(ProductTopology AdjunctionSpace SubspaceTopology RTopology RFuncContinuity Homeomorphisms)