proposition: Lemma f1_helper : forall x : R * R, In S1_Ensemble x -> In UnitInterval_Ensemble (f1 x).
proof: Proof. intros [x y] [H]. unfold f1. simpl. pose proof PI_RGT_0. destruct (acos_bound x). cut (0 <= acos x / (2 * PI) <= 1); constructor. - destruct (Rle_lt_dec y 0); lra. - apply Rdiv_ge_mult; lra. - apply Rdiv_le_mult; lra. Qed.
imports: Coq(Reals.Ratan Lia Lra Logic.IndefiniteDescription Program.Subset) ZornsLemma(Quotients) Topology(ProductTopology AdjunctionSpace SubspaceTopology RTopology RFuncContinuity Homeomorphisms)