Lemma greatest_if_contains_sup (A : hsubtype P) (x : P) : A x -> is_least_upper_bound_subtype A x -> is_greatest_suchthat A x. Proof. intros A_x x_lub. split. - assumption. - apply (pr1 x_lub). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.OrderedSets.WellOrderedSets. Require Import UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo. Require Import UniMath.OrderTheory.Posets.Subposets.