proposition: Lemma meet_idempotent x : x ⊓ x = x.
proof: Proof. assert (le1 : x ⊓ x ≤ x). { refine (meet_lb_l _ _). } assert (le2 : x ≤ x ⊓ x). { refine (meet_glb _ _ _ _ _); apply reflexivity. } refine (antisymmetry _ _ _ le1 le2). Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.semirings HoTT.Classes.theory.lattices