proposition: Lemma valU : Order.join_morphism (val : U -> T).
proof: Proof. by move=> x y; rewrite subK !image_setU !image_set1 set_join2. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)