CoRN.model.partialorder.CRpartialorder

Require Export CRGroupOps.
Require Import PartialOrder.

Example of a Partial Order: <CR, le>

Set Implicit Arguments.

Definition CRmonotone := Default.monotone CRle.
Definition CRantitone := Default.antitone CRle.

Definition CRPartialOrder : PartialOrder :=
makePartialOrder (@st_eq CR) CRle CRmonotone CRantitone
CRle_def CRle_refl CRle_trans (Default.monotone_def _) (Default.antitone_def _).