fact: Definition isupperbound_hprop {I} (p : I -> P) (x:P) : hProp := make_hProp _ (isaprop_isupperbound p x).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.WellOrderedSets UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo