proposition: Lemma monalgOverU c k S : << c *g k >> \in monalgOver S = (c == 0) || (c \in S).
proof: Proof. rewrite qualifE /= msuppU; have [->|nz_c] //= := eqVneq c 0. apply/allP/idP => [h|h x]; last by rewrite in_fset1=> /eqP->; rewrite mcoeffUU. by move: (h k); rewrite mcoeffUU in_fset1 eqxx; apply. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap