x : x ⊔ x = x. Proof. assert (le1 : x ⊔ x ≤ x). { refine (join_lub _ _ _ _ _); apply reflexivity. } assert (le2 : x ≤ x ⊔ x). { refine (join_ub_l _ _). } refine (antisymmetry _ _ _ le1 le2). Qed.
Require Import