proposition: Lemma set_meet0 : set_meet set0 = 1%O :> L.
proof: Proof. by apply/le_anti; rewrite lex1 set_meet_ge_lb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)