proposition: Lemma Rsqr_sum_1_bound_r: forall x y, x²+y²=1 -> -1 <= y <= 1.
proof: Proof. intros. rewrite Rplus_comm in H. now apply Rsqr_sum_1_bound_l in H. Qed.
imports: Coq(Reals.Ratan Lia Lra Logic.IndefiniteDescription Program.Subset) ZornsLemma(Quotients) Topology(ProductTopology AdjunctionSpace SubspaceTopology RTopology RFuncContinuity Homeomorphisms)