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