proposition: Lemma isapropLeastUpperBound (E : hsubtype X) (H : isantisymm (λ x y : X, x <= y)) : isaprop (LeastUpperBound E).
proof: 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.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.QuotientSet UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.BinaryOperations UniMath.Algebra.Apartness UniMath.OrderTheory.Lattice.Lattice