Proposition from_way_below_ideal_completion {I J : rounded_ideal_completion} (Hb : I ≪ J) : ∃ b₁, b₁ ∈ J ∧ I ⊑ principal_ideal b₁. Proof. specialize (Hb (below_ideal_directed_set J) (rounded_ideal_lub_1 J)). revert Hb. use factor_through_squash. { apply propproperty. } intros [[b' Hb'] Hi]. simpl in Hi. assert (H := is_ideal_el (pr2 I)). revert H. use factor_through_squash. { apply propproperty. } intros [b₀ Hb0]. use (hinhpr (b',, (Hb',, _))). - simpl. intros x Hx. apply Hi. exact Hx. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous. Require Import UniMath.OrderTheory.DCPOs.Basis.Algebraic. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Basis.CompactBasis. Require Import UniMath.OrderTheory.DCPOs.Elements.Maximal. Require Import UniMath.OrderTheory.DCPOs.Examples.Products. Require Import UniMath.OrderTheory.DCPOs.Examples.SubDCPO. Require Import UniMath.OrderTheory.DCPOs.Examples.Propositions.