proposition: Lemma set_join0 : set_join set0 = 0%O :> L.
proof: Proof. by apply/le_anti; rewrite le0x set_join_le_ub. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)