proposition: Lemma monalgOverP {g} : reflect (forall m, g@_m \in S) (g \in monalgOver S).
proof: Proof. apply: (iffP allP)=> /= h k; last by rewrite h. by case: msuppP=> [kg|]; rewrite ?rpred0 // (h k). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap