proposition: Lemma set_mulDr (a : U) (B : set U) : set_join B * a = set_join [set x * a | x in B].
proof: Proof. apply/val_inj; rewrite rmorphM/= !omorphSJ/= set_mulDr !image_comp. by congr set_join; apply/eq_imagel => x Bx; rewrite /= rmorphM. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice