proposition: Lemma Rabs_le_1 : forall x y, y >= 0 -> Rabs x <= y -> -y <= x <= y.
proof: Proof. intros. destruct (classic (x < 0)); rewrite Rabs_left in H0 + rewrite Rabs_right in H0; lra. Qed.
imports: Coq(Reals.Ratan Lia Lra Logic.IndefiniteDescription Program.Subset) ZornsLemma(Quotients) Topology(ProductTopology AdjunctionSpace SubspaceTopology RTopology RFuncContinuity Homeomorphisms)