x y z : x < z -> y < z -> x ⊔ y < z. Proof. intros ltxz ltyz. set (disj := cotransitive ltxz (x ⊔ y)). refine (Trunc_rec _ disj); intros [ltxxy|ltxyz]. - set (disj' := cotransitive ltyz (x ⊔ y)). refine (Trunc_rec _ disj'); intros [ltyxy|ltxyz]. + assert (ineqx : x ⊔ y <> x). { apply lt_ne_flip; assumption. } assert (nleyx : ~ (y ≤ x)) by exact (not_contrapositive (join_l x y) ineqx). assert (lexy : x ≤ y). { apply le_iff_not_lt_flip. intros ltyx. refine (nleyx (lt_le _ _ _)). } assert (ineqy : x ⊔ y <> y). { apply lt_ne_flip; assumption. } assert (nlexy : ~ (x ≤ y)) by exact (not_contrapositive (join_r x y) ineqy). assert (leyx : y ≤ x). { apply le_iff_not_lt_flip. intros ltxy. refine (nlexy (lt_le _ _ _)). } assert (eqxy : x = y) by refine (antisymmetry _ _ _ lexy leyx). rewrite <- eqxy in ineqx. destruct (ineqx (join_idempotent x)). + assumption. - assumption. Qed.
Require Import