proposition: Lemma Rsqr_sum_1_bound_l: forall x y, x²+y²=1 -> -1 <= x <= 1.
proof: Proof. intros. apply Rabs_le_1; try lra. rewrite <- Rabs_R1. apply Rsqr_le_abs_0. unfold Rsqr at 2. pose proof (Rle_0_sqr y). lra. Qed.
imports: Coq(Reals.Ratan Lia Lra Logic.IndefiniteDescription Program.Subset) ZornsLemma(Quotients) Topology(ProductTopology AdjunctionSpace SubspaceTopology RTopology RFuncContinuity Homeomorphisms)