x y z : x < y -> x < z -> x < y ⊓ z. Proof. intros ltxy ltxz. set (disj := cotransitive ltxy (y ⊓ z)). refine (Trunc_rec _ disj); intros [ltxyy|ltyzy]. - assumption. - set (disj' := cotransitive ltxz (y ⊓ z)). refine (Trunc_rec _ disj'); intros [ltxyz|ltyzz]. + assumption. + assert (ineqy : y ⊓ z <> y). { apply lt_ne; assumption. } assert (nleyz : ~ (y ≤ z)) by exact (not_contrapositive (meet_l y z) ineqy). assert (lezy : z ≤ y). { apply le_iff_not_lt_flip. intros ltzy. refine (nleyz (lt_le _ _ _)). } assert (ineqz : y ⊓ z <> z). { apply lt_ne; assumption. } assert (nlezy : ~ (z ≤ y)) by exact (not_contrapositive (meet_r y z) ineqz). assert (leyz : y ≤ z). { apply le_iff_not_lt_flip. intros ltzy. refine (nlezy (lt_le _ _ _)). } assert (eqyz : y = z) by refine (antisymmetry _ _ _ leyz lezy). rewrite <- eqyz in ineqy. destruct (ineqy (meet_idempotent y)). Qed.
Require Import