proposition: Lemma circle_cover_image t : In S1_Ensemble (circle_cover t).
proof: Proof. constructor. simpl. rewrite Rplus_comm. apply sin2_cos2. Qed.
imports: Coq(Reals.Ratan Lia Lra Logic.IndefiniteDescription Program.Subset) ZornsLemma(Quotients) Topology(ProductTopology AdjunctionSpace SubspaceTopology RTopology RFuncContinuity Homeomorphisms)