proposition: Lemma boolset_lattice : lattice boolset.
proof: Proof. use make_lattice. - exact andb. - exact orb. - apply make_dirprod; [apply make_dirprod|apply make_dirprod; [apply make_dirprod|apply make_dirprod]]. + intros ? ? ?; apply andb_is_associative. + intros ? ?; apply andb_is_commutative. + intros ? ? ?; apply orb_is_associative. + intros ? ?; apply orb_is_commutative. + intros b1 b2; abstract (induction b1, b2; reflexivity). + intros b1 b2; abstract (induction b1, b2; reflexivity). Defined.
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