proposition: Lemma set_joinU_le S S' x : set_join S <= x -> set_join S' <= x -> set_join (S `|` S') <= x.
proof: Proof. move=> jSx jS'x; apply: set_join_le_ub => y [] Sy. - move: jSx; exact/le_trans/set_join_ub. - move: jS'x; exact/le_trans/set_join_ub. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)