Proposition way_below_prod_pr1 {xy₁ xy₂ : prod_dcpo X Y} (p : xy₁ ≪ xy₂) : pr1 xy₁ ≪ pr1 xy₂. Proof. intros D q. pose (D' := prod_directed_set_dcpo D (directed_set_from_basis BY (pr2 xy₂))). assert (HD : xy₂ ⊑ ⨆ D'). { unfold D'. rewrite prod_dcpo_lub'. rewrite approximating_basis_lub. exact (q ,, refl_dcpo _). } assert (H := p D' HD). revert H. use factor_through_squash. { apply propproperty. } intro H. induction H as [ i H ]. exact (hinhpr (pr1 i ,, pr1 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.