Definition pr1GreatestLowerBound {E : hsubtype X} : GreatestLowerBound E → X := pr1.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.BinaryOperations