fact: Definition dense_regular (y : Y) : Complete X := mkRegularFunction (app_inverse f y (exist (Qlt 0) (1#1) eq_refl) : X) (dense_regular_prf y).
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