fact: Definition least_of_family {I} (p : I -> P) := ∑ i : I, islowerbound p (p i).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.WellOrderedSets UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo