proposition: Lemma finsupp_sub (S : {fset K}) (h : S -> V) : finsupp [fsfun[key] a : S => h a | default a] `<=` S.
proof: Proof. apply/fsubsetP => a; rewrite mem_finsupp unlock /=. by case: insubP => //=; rewrite eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)