IsJoinSemiLattice L. Proof. repeat split. - apply _. - intros x y z. apply (antisymmetry (≤)). + apply join_lub. * apply join_ub_3_l. * apply join_lub. ** apply join_ub_3_m. ** apply join_ub_3_r. + apply join_lub. * apply join_lub. ** apply join_ub_3_assoc_l. ** apply join_ub_3_assoc_m. * apply join_ub_3_assoc_r. - intros x y. apply (antisymmetry (≤)); apply join_lub; first [apply join_ub_l | apply join_ub_r]. - intros x. red. apply (antisymmetry (≤)). + apply join_lub; apply reflexivity. + apply join_ub_l. Qed.
Require Import