proposition: Lemma msuppC (c : G) : msupp c%:MP = (if c == 0 then fset0 else [fset 1%M]) :> {fset K}.
proof: Proof. exact/msuppU. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap