fact: Definition default_meet_sl_le `{IsMeetSemiLattice L} : Le L := fun x y => x ⊓ y = x.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.semirings HoTT.Classes.theory.lattices