proposition: Lemma set_join_le_incl S S' : S `<=` S' -> set_join S <= set_join S'.
proof: Proof. move=> SS'; apply: set_join_le_ub => x Sx; exact/set_join_ub/SS'. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)