Lemma boolset_lattice_is_complemented : complemented_structure (make_bounded_lattice boolset_lattice_is_bounded). Proof. intros b. exists (negb b). use make_dirprod. - abstract (induction b; reflexivity). - abstract (induction b; reflexivity). Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Bool. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded. Require Import UniMath.OrderTheory.Lattice.Distributive. Require Import UniMath.OrderTheory.Lattice.Complement. Require Import UniMath.OrderTheory.Lattice.Boolean.