Definition CRLattice : Lattice :=
makeLattice CRPartialOrder (ucFun2 CRmin) (ucFun2 CRmax)
 CRmin_lb_l CRmin_lb_r CRmin_glb CRmax_ub_l CRmax_ub_r CRmax_lub.

Section CRLattice.

Let CRlat := CRLattice.


Definition CRmin_comm : forall x y : CR, CRmin x y == CRmin y x := @meet_comm CRlat.
Definition CRmin_assoc : forall x y z : CR, CRmin x (CRmin y z) == CRmin (CRmin x y) z:=
 @meet_assoc CRlat.
Definition CRmin_idem : forall x : CR, CRmin x x == x := @meet_idem CRlat.
Definition CRle_min_l : forall x y : CR, x <= y <-> CRmin x y == x := @le_meet_l CRlat.
Definition CRle_min_r : forall x y : CR, y <= x <-> CRmin x y == y := @le_meet_r CRlat.
Definition CRmin_monotone_r : forall a : CR, CRmonotone (CRmin a) :=
 @meet_monotone_r CRlat.
Definition CRmin_monotone_l : forall a : CR, CRmonotone (fun x => CRmin x a) :=
 @meet_monotone_l CRlat.
Definition CRmin_le_compat :
 forall w x y z : CR, w <= y -> x <= z -> CRmin w x <= CRmin y z :=
 @meet_le_compat CRlat.

Definition CRmax_comm : forall x y : CR, CRmax x y == CRmax y x := @join_comm CRlat.
Definition CRmax_assoc : forall x y z : CR, CRmax x (CRmax y z) == CRmax (CRmax x y) z:=
 @join_assoc CRlat.
Definition CRmax_idem : forall x : CR, CRmax x x == x := @join_idem CRlat.
Definition CRle_max_l : forall x y : CR, y <= x <-> CRmax x y == x := @le_join_l CRlat.
Definition CRle_max_r : forall x y : CR, x <= y <-> CRmax x y == y := @le_join_r CRlat.
Definition CRmax_monotone_r : forall a : CR, CRmonotone (CRmax a) :=
 @join_monotone_r CRlat.
Definition CRmax_monotone_l : forall a : CR, CRmonotone (fun x => CRmax x a) :=
 @join_monotone_l CRlat.
Definition CRmax_le_compat :
 forall w x y z : CR, w<=y -> x<=z -> CRmax w x <= CRmax y z :=
 @join_le_compat CRlat.

Definition CRmin_max_absorb_l_l : forall x y : CR, CRmin x (CRmax x y) == x :=
 @meet_join_absorb_l_l CRlat.
Definition CRmax_min_absorb_l_l : forall x y : CR, CRmax x (CRmin x y) == x :=
 @join_meet_absorb_l_l CRlat.
Definition CRmin_max_absorb_l_r : forall x y : CR, CRmin x (CRmax y x) == x :=
 @meet_join_absorb_l_r CRlat.
Definition CRmax_min_absorb_l_r : forall x y : CR, CRmax x (CRmin y x) == x :=
 @join_meet_absorb_l_r CRlat.
Definition CRmin_max_absorb_r_l : forall x y : CR, CRmin (CRmax x y) x == x :=
 @meet_join_absorb_r_l CRlat.
Definition CRmax_min_absorb_r_l : forall x y : CR, CRmax (CRmin x y) x == x :=
 @join_meet_absorb_r_l CRlat.
Definition CRmin_max_absorb_r_r : forall x y : CR, CRmin (CRmax y x) x == x :=
 @meet_join_absorb_r_r CRlat.
Definition CRmax_min_absorb_r_r : forall x y : CR, CRmax (CRmin y x) x == x :=
 @join_meet_absorb_r_r CRlat.

Definition CRmin_max_eq : forall x y : CR, CRmin x y == CRmax x y -> x == y :=
 @meet_join_eq CRlat.


End CRLattice.