proposition: Proposition from_way_below_ideal_completion {I J : rounded_ideal_completion} (Hb : I ≪ J) : ∃ b₁, b₁ ∈ J ∧ I ⊑ principal_ideal b₁.
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Continuous UniMath.OrderTheory.DCPOs.Basis.Algebraic UniMath.OrderTheory.DCPOs.Basis.Basis UniMath.OrderTheory.DCPOs.Basis.CompactBasis UniMath.OrderTheory.DCPOs.Elements.Maximal UniMath.OrderTheory.DCPOs.Examples.Products UniMath.OrderTheory.DCPOs.Examples.SubDCPO UniMath.OrderTheory.DCPOs.Examples.Propositions