Proposition to_way_below_ideal_completion {I J : rounded_ideal_completion} (b₁ : B) (Hb1 : b₁ ∈ J) (HI : I ⊑ principal_ideal b₁) : I ≪ J. 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.
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.