fact: Record PartialOrder : Type := { po_car :> RSetoid ; le : po_car -> po_car -> Prop ; monotone : (po_car -> po_car) -> Prop ; antitone : (po_car -> po_car) -> Prop ; po_proof : is_PartialOrder (@st_eq po_car) le monotone antitone }.
imports: CoRN.algebra.RSetoid