proposition: Lemma fsfun_fun (S : {fset K}) (h : K -> V) (x : K) : [fsfun[key] a in S => h a | default a] x = if x \in S then h x else (default x).
proof: Proof. by rewrite fsfun_ffun; case: insubP => //= [u -> ->|/negPf ->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)