proposition: Lemma join_idempotent x : x ⊔ x = x.
proof: 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.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.semirings HoTT.Classes.theory.lattices