proposition: Lemma set_mulDr a (B : set D) : set_join B * a = set_join [set x * a | x in B].
proof: Proof. by rewrite mulrC set_mulDl; apply: f_equal; rewrite predeqP => x; split; (move=> -[y Hy <-]; exists y; [|rewrite mulrC]). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice