Lemma isapropGreatestLowerBound (E : hsubtype X) (H : isantisymm (λ x y : X, x >= y)) : isaprop (GreatestLowerBound E). Proof. intros x y. apply (iscontrweqf (X := (pr1 x) = (pr1 y))). - apply invweq, subtypeInjectivity. intro t. apply isapropdirprod. apply impred_isaprop ; intro. apply isapropimpl. now apply pr2. apply impred_isaprop ; intro. apply isapropimpl. now apply pr2. - assert (Heq : (pr1 x) = (pr1 y)). { apply H. now apply (pr2 (pr2 x)), (pr1 (pr2 y)). now apply (pr2 (pr2 y)), (pr1 (pr2 x)). } rewrite <- Heq. apply iscontrloopsifisaset. apply pr2. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.BinaryOperations