Lemma lubpreservesorder {X : Poset} {I : UU} (u v : I -> X) : (∏ (i : I), u i ≤ v i) -> ∏ (lu lv : X), islub u lu -> islub v lv -> lu ≤ lv. Proof. intros ineqs lu lv islubu islubv. eapply islub_isleast. - exact islubu. - intro i. eapply istrans_posetRelation. + exact (ineqs i). + apply (islub_isupperbound v islubv). Qed.
Require Import UniMath.Foundations.All.