proposition: Lemma monalgOver_mulr_closed : mulr_closed (monalgOver S).
proof: Proof. split=> [|g1 g2 /monalgOverP Sg1 /monalgOverP sS2]. by rewrite monalgOver1. apply/monalgOverP=> m; rewrite mcoeffMl rpred_sum //=. move=> k1 _; rewrite rpred_sum // => k2 _. by case: eqP; rewrite ?mulr0n (rpred0, rpredM). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap