proposition: Lemma finsuppP f k : fsfun_spec f k (f k) (k \in finsupp f).
proof: Proof. have [kf|kNf] := boolP (_ \in _); first by constructor. by rewrite fsfun_dflt // ; constructor. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)