Definition complement_to_element {x : X} (y : complement x) : X := pr1 y.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.Foundations.Sets. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.