fact: Definition complement_bottom_axiom (x : X) (y : complement x) : x ⊗ y = ⊥ := dirprod_pr2 (pr2 y).
imports: UniMath.Foundations.Preamble UniMath.Foundations.Sets UniMath.OrderTheory.Lattice.Lattice UniMath.OrderTheory.Lattice.Bounded