fact: Definition min x y := match total le x y with | inr _ => y | inl _ => x end.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.semirings HoTT.Classes.theory.lattices