proposition: Lemma dense_regular_prf (y : Y) : is_RegularFunction_noInf _ (app_inverse f y : Qpos → X).
proof: Proof. intros ε1 ε2. simpl. eapply ball_triangle. now eapply dense_inverse. now eapply ball_sym, dense_inverse. Qed.
imports: CoRN.metric2.Metric CoRN.model.totalorder.QposMinMax Coq.Setoids.Setoid CoRN.stdlib_omissions.Q CoRN.model.totalorder.QMinMax CoRN.metric2.Complete CoRN.metric2.Prelength MathClasses.interfaces.abstract_algebra