proposition: Fact comp_is_set_join_morphism : set_join_morphism (f \o g).
proof: Proof. by move=> B; rewrite /= !omorphSJ image_comp. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)