proposition: Lemma f_inv_helper (x y : UnitInterval) : SpaceAdjunction (Couple U0 U1) x y -> (fun x => exist _ (circle_cover (subspace_inc _ x)) (circle_cover_image _)) x = (fun x => exist _ (circle_cover (subspace_inc _ x)) (circle_cover_image _)) y.
proof: Proof. intros. destruct x as [x Hx]. destruct y as [y Hy]. apply subset_eq. simpl. red in H. destruct H as [|[]]. - inversion H; subst; clear H. reflexivity. - inversion H; subst; clear H; inversion H0; subst; clear H0; try reflexivity. all: unfold circle_cover. all: rewrite Rmult_0_r. all: rewrite Rmult_1_r. all: rewrite cos_0, sin_0. all: rewrite Rtrigo1.cos_2PI. all: rewrite Rtrigo1.sin_2PI. all: reflexivity. Qed.
imports: Coq(Reals.Ratan Lia Lra Logic.IndefiniteDescription Program.Subset) ZornsLemma(Quotients) Topology(ProductTopology AdjunctionSpace SubspaceTopology RTopology RFuncContinuity Homeomorphisms)