Proposition poset_to_bounded_lattice_laws : bounded_latticeop poset_to_lattice bot top. Proof. repeat split ; intro x ; cbn ; use isantisymm_posetRelation. - use max_op_le. * apply is_min_min_el. * apply isrefl_posetRelation. - apply max_op_r. - apply min_op_r. - use le_min_op. * apply is_max_max_el. * apply isrefl_posetRelation. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.