proposition: Proposition way_below_prod_pr1 {xy₁ xy₂ : prod_dcpo X Y} (p : xy₁ ≪ xy₂) : pr1 xy₁ ≪ pr1 xy₂.
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.ScottTopology UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Basis UniMath.OrderTheory.DCPOs.Basis.Continuous UniMath.OrderTheory.DCPOs.Elements.Maximal