Proposition way_below_prod_pr2 {xy₁ xy₂ : prod_dcpo X Y} (p : xy₁ ≪ xy₂) : pr2 xy₁ ≪ pr2 xy₂. Proof. intros D q. pose (D' := prod_directed_set_dcpo (directed_set_from_basis BX (pr1 xy₂)) D). assert (HD : xy₂ ⊑ ⨆ D'). { unfold D'. rewrite prod_dcpo_lub'. rewrite approximating_basis_lub. exact (refl_dcpo _ ,, q). } assert (H := p D' HD). revert H. use factor_through_squash. { apply propproperty. } intro H. induction H as [ i H ]. exact (hinhpr (pr2 i ,, pr2 H)). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. 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.ScottTopology. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous. Require Import UniMath.OrderTheory.DCPOs.Elements.Maximal.