fact: Definition min_case x y (P:A -> Type) (Hx : le x y -> P x) (Hy : le y x -> P y) : P (min x y) := match (le_total x y) as s return P (if s then x else y) with | left p => Hx p | right p => Hy p end.
imports: Coq.Setoids.Setoid CoRN.order.Lattice