proposition: 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: Proof. intros A_x x_lub. split. - assumption. - apply (pr1 x_lub). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.WellOrderedSets UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo