proposition: Lemma join_le x y z : x <= z -> y <= z -> join x y <= z.
proof: Proof. by move=> Hx Hy; apply: set_joinU_le; rewrite set_join1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)