Proposition poset_to_lattice_laws : islatticeop (min_op min) (max_op max). Proof. repeat split. - intros x y z. use isantisymm_posetRelation. + use le_min_op. * refine (istrans_posetRelation _ _ _ _ _ _) ; [ apply min_op_l | ]. apply min_op_l. * use le_min_op. ** refine (istrans_posetRelation _ _ _ _ _ _) ; [ apply min_op_l | ]. apply min_op_r. ** apply min_op_r. + use le_min_op. * use le_min_op. ** apply min_op_l. ** refine (istrans_posetRelation _ _ _ _ _ _) ; [ apply min_op_r | ]. apply min_op_l. * refine (istrans_posetRelation _ _ _ _ _ _) ; [ apply min_op_r | ]. apply min_op_r. - intros x y. use isantisymm_posetRelation. + use le_min_op. * apply min_op_r. * apply min_op_l. + use le_min_op. * apply min_op_r. * apply min_op_l. - intros x y z. use isantisymm_posetRelation. + use max_op_le. * use max_op_le. ** apply max_op_l. ** refine (istrans_posetRelation _ _ _ _ _ _) ; [ | apply max_op_r ]. apply max_op_l. * refine (istrans_posetRelation _ _ _ _ _ _) ; [ | apply max_op_r ]. apply max_op_r. + use max_op_le. * refine (istrans_posetRelation _ _ _ _ _ _) ; [ | apply max_op_l ]. apply max_op_l. * use max_op_le. ** refine (istrans_posetRelation _ _ _ _ _ _) ; [ | apply max_op_l ]. apply max_op_r. ** apply max_op_r. - intros x y. use isantisymm_posetRelation. + use max_op_le. * apply max_op_r. * apply max_op_l. + use max_op_le. * apply max_op_r. * apply max_op_l. - intros x y. use isantisymm_posetRelation. + apply min_op_l. + use le_min_op. * apply isrefl_posetRelation. * apply max_op_l. - intros x y. use isantisymm_posetRelation. + apply max_op_le. * apply isrefl_posetRelation. * apply min_op_l. + use max_op_l. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.