proposition: Proposition to_way_below_ideal_completion {I J : rounded_ideal_completion} (b₁ : B) (Hb1 : b₁ ∈ J) (HI : I ⊑ principal_ideal b₁) : I ≪ J.
proof: Proof. intros D HJ. assert (HbJ : principal_ideal b₁ ≪ J). { apply principal_ideal_way_below, Hb1. } specialize (HbJ D HJ). revert HbJ. use factor_through_squash. { apply propproperty. } intros [i Hi]. use (hinhpr (i,, _)). exact (trans_dcpo HI Hi). 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