fact: Definition isOneSided (S : hq → hProp) : UU := ((∃ r : hq, S r) ∧ (∃ r : hq, ¬ S r)) × (∏ r : hq, S r → ∃ q : hq, S q ∧ hqlth r q) × (∏ r s : hq, hqlth r s → S r ∨ ¬ S s).
imports: UniMath.NumberSystems.RationalNumbers UniMath.RealNumbers.Prelim UniMath.RealNumbers.NonnegativeRationals UniMath.RealNumbers.NonnegativeReals