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